@inproceedings{ATPEtypes07,
author = "Hongwei Xi",
title = {{Attributive Types for Proof Erasure}},
booktitle = "post-workshop Proceedings of TYPES 2007",
publisher = "Springer-Verlag LNCS 4941",
year = "2007",
pages = "188-202",
abstract = {{
Proof erasure plays an essential role in the paradigm of programming with
theorem proving. In this paper, we introduce a form of {\em 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.
}}
}