Abstract
It is demonstrated how a dependently typed lambda calculus (a logical framework) can be formalised inside a language with inductive-recursive families. The formalisation does not use raw terms; the well-typed terms are defined directly. It is hence impossible to create ill-typed terms.
As an example of programming with strong invariants, and to show that the formalisation is usable, normalisation is proved. Moreover, this proof seems to be the first formal account of normalisation by evaluation for a dependently typed language.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abel, A., Altenkirch, T.: A predicative analysis of structural recursion. Journal of Functional Programming 12(1), 1–41 (2002)
Abel, A., Aehlig, K., Dybjer, P.: Normalization by evaluation for Martin-Löf type theory with one universe. Submitted for publication (2007)
Altenkirch, T., Chapman, J.: Tait in one big step. In: MSFP 2006 (2006)
Adams, R.: Formalized metatheory with terms represented by an indexed family of types. In: TYPES 2004. LNCS, vol. 3839, pp. 1–16. Springer, Heidelberg (2004)
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)
Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed λ-calculus. In: LICS 1991, pp. 203–211 (1991)
Barras, B., Werner, B.: Coq in Coq. Unpublished (1997)
Coquand, T., Dybjer, P.: Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science 7(1), 75–94 (1997)
Coquand, C.: A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions. Higher-Order and Symbolic Computation 15, 57–90 (2002)
Danielsson, N.A.: Personal web page. available (2007), at http://www.cs.chalmers.se/~nad/
Dybjer, P., Setzer, A.: Indexed induction-recursion. Journal of Logic and Algebraic Programming 66(1), 1–49 (2006)
Dybjer, P.: Internal type theory. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 120–134. Springer, Heidelberg (1996)
McBride, C.: Beta-normalization for untyped lambda-calculus (unpublished program)
McBride, C.: Type-preserving renaming and substitution (unpublished)
Martin-Löf, P.: An intuitionistic theory of types: Predicative part. In: Logic Colloquium ’73, pp. 73–118. North-Holland, Amsterdam (1975)
Martin-Löf, P.: Normalization by evaluation and by the method of computability. Lecture series given at Logikseminariet Stockholm–Uppsala (2004)
Mitchell, J.C., Moggi, E.: Kripke-style models for typed lambda calculus. Annals of Pure and Applied Logic 51, 99–124 (1991)
McBride, C., McKinna, J.: The view from the left. Journal of Functional Programming 14(1), 69–111 (2004)
McKinna, J., Pollack, R.: Some lambda calculus and type theory formalized. Journal of Automated Reasoning 23(3), 373–409 (1999)
McKinna, J., Wright, J.: A type-correct, stack-safe, provably correct expression compiler in Epigram. Accepted for publication in the Journal of Functional Programming (2006)
Norell, U.: AgdaLight home page. available (2007), at http://www.cs.chalmers.se/~ulfn/agdaLight/
Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf’s Type Theory, An Introduction. Oxford University Press, Oxford (1990)
Pašalić, E., Linger, N.: Meta-programming with typed object-language representations. In: Karsai, G., Visser, E. (eds.) GPCE 2004. LNCS, vol. 3286, pp. 136–167. Springer, Heidelberg (2004)
Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: POPL 2003, pp. 224–235 (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Danielsson, N.A. (2007). A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family. In: Altenkirch, T., McBride, C. (eds) Types for Proofs and Programs. TYPES 2006. Lecture Notes in Computer Science, vol 4502. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74464-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-74464-1_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74463-4
Online ISBN: 978-3-540-74464-1
eBook Packages: Computer ScienceComputer Science (R0)