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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Danielsson, N. A. (2007). A formalisation of a dependently typed language as an inductive-recursive family. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4502 LNCS, pp. 93–109). Springer Verlag. https://doi.org/10.1007/978-3-540-74464-1_7
Mendeley helps you to discover research relevant for your work.