A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family

A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
Proglog meeting, 2007-01-31. Slides slightly edited. [pdf, pdf (n-up)]

Abstract

In 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:
* Explicit substitutions.
* The code is structurally recursive.
* Full normalisation (not just to weak head normal form).
* Equality checker.
* Type checker.