Attributive Types for Proof Erasure

Abstract. Proof erasure plays an essential role in the paradigm of programming with theorem proving. In this paper, we introduce a form of attributive types that carry an attribute to determine whether expressions assigned such types are eligible for erasure before run-time. We formalize a type system to support this form of attributive types and then establish its soundness. In addition, we outline an extension of the developed type system with dependent types and present some examples to illustrate its use in practice.

• Type: Conference
• Year: 2007
• Where: TYPES
• Authors: Hongwei Xi
• Keywords: Attributive Types, Essential Role, Formal Methods, Proof Erasure, TYPES 2007