@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",

}