A Well-typed Interpreter for a Dependently Typed Language

A Well-typed Interpreter for a Dependently Typed Language
Fun in the Afternoon, Nottingham, 2007-02-21. [pdf, pdf (n-up)]

Abstract

GADTs are often introduced with the "well-typed interpreter" example. A simple programming language is encoded as a GADT in such a way that only well-typed terms can be defined, and then an interpreter which cannot get stuck is implemented.

I'll show how to do this for a dependently typed lambda calculus, in the dependently typed meta-language AgdaLight. To accomplish this I'll use inductive-recursive families, a generalisation of GADTs.