| Attributive Types for Proof Erasure ⋆ (2008) | |||||||||||||||
Abstract | |||||||||||||||
| 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. 1 | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||