Sciweavers

Share
TYPES
2007
Springer

Attributive Types for Proof Erasure

9 years 2 months ago
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.
Hongwei Xi
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where TYPES
Authors Hongwei Xi
Comments (0)
books