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

Documents

  • Coqpts2

    Submitted manuscript, 54.2 KB, application/x-dvi

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

Publication series

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

Conference

ConferenceTYPES 2004
CountryUnited Kingdom
CityJouy-en-Josas
Period15/12/0418/12/04
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 398716