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

Published

Standard

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

Harvard

Adams, R 2006, Formalized Metatheory with Terms Represented by an Indexed Family of Types. in J-C Filliatre, C Paulin-Mohring & B Werner (eds), Types for Proofs and Programs. vol. 3839, Lecture Notes in Computer Science, Springer, pp. 1-16, TYPES 2004, Jouy-en-Josas, United Kingdom, 15/12/04. https://doi.org/10.1007/11617990_1

APA

Adams, R. (2006). Formalized Metatheory with Terms Represented by an Indexed Family of Types. In J-C. Filliatre, C. Paulin-Mohring, & B. Werner (Eds.), Types for Proofs and Programs (Vol. 3839, pp. 1-16). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/11617990_1

Vancouver

Adams R. Formalized Metatheory with Terms Represented by an Indexed Family of Types. In Filliatre J-C, Paulin-Mohring C, Werner B, editors, Types for Proofs and Programs. Vol. 3839. Springer. 2006. p. 1-16. (Lecture Notes in Computer Science). https://doi.org/10.1007/11617990_1

Author

Adams, Robin. / Formalized Metatheory with Terms Represented by an Indexed Family of Types. Types for Proofs and Programs. editor / Jean-Christophe Filliatre ; Christine Paulin-Mohring ; Benjamin Werner. Vol. 3839 Springer, 2006. pp. 1-16 (Lecture Notes in Computer Science).

BibTeX

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

}

RIS

TY - GEN

T1 - Formalized Metatheory with Terms Represented by an Indexed Family of Types

AU - Adams, Robin

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

U2 - 10.1007/11617990_1

DO - 10.1007/11617990_1

M3 - Conference contribution

SN - 978-3-540-31428-8

VL - 3839

T3 - Lecture Notes in Computer Science

SP - 1

EP - 16

BT - Types for Proofs and Programs

A2 - Filliatre, Jean-Christophe

A2 - Paulin-Mohring, Christine

A2 - Werner, Benjamin

PB - Springer

T2 - TYPES 2004

Y2 - 15 December 2004 through 18 December 2004

ER -