Abstract
It is possible to represent the terms of a syntax with binding constructors by a family of types, indexed by the free variables that may occur. This approach has been used several times for the study of syntax and substitution, but never for the formalization of the metatheory of a typing system. We describe a recent formalization of the metatheory of Pure Type Systems in Coq as an example of such a formalization. In general, careful thought is required as to how each definition and theorem should be stated, usually in an unfamiliar ‘big-step’ form; but, once the correct form has been found, the proofs are very elegant and direct.
This is a preview of subscription content, log in via an institution to check access.
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
Bellegarde, F., Hook, J.: Subsitution: A formal methods case study using monads and transformations. Sci. Comput. Program. 23, 287–311 (1994)
Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 453–468. Springer, Heidelberg (1999)
Bird, R.S., Paterson, R.: de Bruijn notation as a nested datatype. J. Functional Programming 9, 77–91 (1999)
Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. II. Oxford University Press, Oxford (1992)
van Benthem Jutting, L.S.: Typing in pure type systems. Information and Computation 105, 30–41 (1993)
McKinna, J., Pollack, R.: Some lambda calculus and type theory formalized. J. Autom. Reasoning 23, 373–409 (1999)
Barras, B.: Auto-validation d’un sysème de preuves avec familles inductives. PhD thesis, Université Paris 7 (1999)
Letouzey, P.: Vectors. Message to Coq-Club mailing list (2004), http://pauillac.inria.fr/pipermail/coq-club/2004/001265.html
Adams, R.: A formalization of the theory of PTSs in Coq (2005), Available online at, http://www.cs.rhul.ac.uk/~robin/coqPTS/docu.dvi
Adams, R.: Pure type systems with judgemental equality. Accepted for publication in the Journal of Functional Programming
Barras, B.: A formalization of the calculus of constructions, Web page, http://coq.inria.fr/contribs/coq-in-coq.html
Pfenning, F., Elliot, C.: Higher-order abstract syntax. In: PLDI 1988: Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, pp. 199–208. ACM Press, New York (1988)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13, 341–363 (2002)
Stehr, M.O.: CINNI: A generic calculus of explicit substitutions and its application to lambda-, sigma- and pi-calculi. In: Third International Workshop on Rewriting Logic and its Applications (WRLA 2000). Electronic Notes in Theoretical Computer Science, vol. 36, Kanazawa, Japan, September 18-20. Elsevier, Amsterdam (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Adams, R. (2006). Formalized Metatheory with Terms Represented by an Indexed Family of Types. In: Filliâtre, JC., Paulin-Mohring, C., Werner, B. (eds) Types for Proofs and Programs. TYPES 2004. Lecture Notes in Computer Science, vol 3839. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11617990_1
Download citation
DOI: https://doi.org/10.1007/11617990_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31428-8
Online ISBN: 978-3-540-31429-5
eBook Packages: Computer ScienceComputer Science (R0)