@inproceedings{5b72601ea6b847c984ced90a7bd85575,
title = "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.",
author = "Robin Adams",
year = "2006",
doi = "10.1007/11617990_1",
language = "English",
isbn = "978-3-540-31428-8",
volume = "3839",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "1--16",
editor = "Jean-Christophe Filliatre and Christine Paulin-Mohring and Benjamin Werner",
booktitle = "Types for Proofs and Programs",
note = "TYPES 2004 ; Conference date: 15-12-2004 Through 18-12-2004",
}