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

A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
Nils Anders Danielsson
Types for Proofs and Programs, International Workshop, TYPES 2006, Revised Selected Papers, LNCS 4502, 2007. Copyright © Springer-Verlag Berlin Heidelberg 2007. [pdf, accompanying code]

Abstract

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.

Erratum

The 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.