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 @Val is not defined in the same way in the paper and in the accompanying AgdaLight code. In the accompanying code the combinator is defined using pattern matching on the result of eq⊢eq⋆ eq. The code in the paper is not type-correct. Nils Anders DanielssonLast updated Mon May 13 12:16:14 UTC 2013. |