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.
This work is partially supported by NSF grants no. CCR-0229480 and no. CCF-0702665.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)
Constable, R.L., et al.: Implementing Mathematics with the NuPrl Proof Development System, p. 299. Prentice-Hall, Englewood Cliffs, New Jersey (1986)
Chen, C., Xi, H.: Combining Programming with Theorem Proving. In: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, Tallinn, Estonia, September 2005, pp. 66–77 (2005)
Dantzig, G.B., Eaves, B.C.: Fourier-Motzkin elimination and its dual. Journal of Combinatorial Theory (A) 14, 288–297 (1973)
Dowek, G., Felty, A., Herbelin, H., Huet, G., Murthy, C., Parent, C., Paulin-Mohring, C., Werner, B.: The Coq proof assistant user’s guide. Rapport Technique 154, INRIA, Rocquencourt, France, Version 5.8 (1993)
Jouvelot, P., Gifford, D.K.: Algebraic reconstruction of types and effects. In: Proceedings of 18th ACM SIGPLAN Symposium on Principles of Programming Languages, January 1991, pp. 303–310 (1991)
Letouzey, P.: A New Extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, Springer, Heidelberg (2003)
Martin-Löf, P.: Intuitionistic Type Theory, Bibliopolis, Naples, Italy, p. 91 (1984) ISBN88-7088-105-9
Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf’s Type Theory. International Series of Monographs on Computer Science, vol. 7, p. 221. Clarendon Press, Oxford (1990)
Pfenning, F.: Intentionality, Extentionality and Proof Irrelevance in Modal Type Theory. In: Proceedings of 16th IEEE Symposium on Logic in Computer Science, Boston, June 2001, pp. 221–230 (2001)
Paulin-Mohring, C.: Extraction de programmes dans le Calcul des Constructions. Thèse de doctorat, Université de Paris VII, Paris, France (1989)
Xi, H.: The ATS Programming Language. Available at: http://www.ats-lang.org/
Xi, H.: Dependent Types for Program Termination Verification. Journal of Higher-Order and Symbolic Computation 15(1), 91–132 (2002)
Xi, H.: Applied Type System (extended abstract). In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 394–408. Springer, Heidelberg (2004)
Xi, H.: Dependent ML: an approach to practical programming with dependent types. Journal of Functional Programming 17(2), 215–286 (2007)
Xi, H., Pfenning, F.: Dependent Types in Practical Programming. In: Proceedings of 26th ACM SIGPLAN Symposium on Principles of Programming Languages, San Antonio, Texas, January 1999, pp. 214–227. ACM press, New York (1999)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Xi, H. (2008). Attributive Types for Proof Erasure. In: Miculan, M., Scagnetto, I., Honsell, F. (eds) Types for Proofs and Programs. TYPES 2007. Lecture Notes in Computer Science, vol 4941. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68103-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-68103-8_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68084-0
Online ISBN: 978-3-540-68103-8
eBook Packages: Computer ScienceComputer Science (R0)