Formalized Metatheory with Terms Represented by an Indexed Family of Types. / Adams, Robin.

Types for Proofs and Programs. ed. / Jean-Christophe Filliatre; Christine Paulin-Mohring; Benjamin Werner. Vol. 3839 Springer, 2006. p. 1-16 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingConference contribution



  • Coqpts2

    Submitted manuscript, 54.2 KB, application/x-dvi


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.
Original languageEnglish
Title of host publicationTypes for Proofs and Programs
EditorsJean-Christophe Filliatre, Christine Paulin-Mohring, Benjamin Werner
Number of pages16
ISBN (Print)978-3-540-31428-8
Publication statusPublished - 2006
EventTYPES 2004 - Jouy-en-Josas, United Kingdom
Duration: 15 Dec 200418 Dec 2004

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


ConferenceTYPES 2004
Country/TerritoryUnited Kingdom
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 398716