Adams, Robin (2006) Formalized Metatheory with Terms Represented by an Indexed Family of Types In: Types for Proofs and Programs. Springer.
Full text access: Open
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.
This is a Submitted version This version's date is: 2006 This item is not peer reviewed
https://repository.royalholloway.ac.uk/items/2b2771df-400c-591e-393d-8359dc27989e/3/
Deposited by Research Information System (atira) on 27-Jan-2013 in Royal Holloway Research Online.Last modified on 27-Jan-2013