A Formalisation of a Dependently Typed Language as an Inductive-Recursive FamilyA Formalisation of a Dependently Typed Language as an Inductive-Recursive Family AbstractIn this work 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. By proving normalisation, it is shown that the formalisation is usable. Moreover, this proof seems to be the first formal account of normalisation by evaluation for a dependently typed language. New since last time: Last updated Sat Feb 16 14:24:14 UTC 2008. |