Formalized Metatheory with Terms Represented by an Indexed Family of Types

Abstract

We describe a recent formalization of several results from the metatheory of Pure Type Systems (PTSs) in Coq, including Subject Reduction, Uniqueness of Types in a functional PTS, and the difficult proof of Strengthening. The terms of the PTS are represented by an inductive family of types: "term n" is the type of all terms with at most n free variables. This representation of terms has often been used to study syntax and substitution, but not the metatheory of a formal system. We show how it requires many metatheorems to be stated in a somewhat unfamiliar "big-step" form, but then allows for very elegant and direct proofs.