## A Formalisation of a Dependently Typed Language as an Inductive-Recursive FamilyA Formalisation of a Dependently Typed Language as an Inductive-Recursive Family ## AbstractIt 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. ## ErratumThe cast case of the combinator eq. The code in the
paper is not type-correct.
_{⊢}eq_{⋆} eqLast updated Mon May 13 12:16:14 UTC 2013. |