Formalized Metatheory with Terms Represented by an Indexed Family of Types

Robin Adams

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

60 Downloads (Pure)

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
Country/TerritoryUnited Kingdom
CityJouy-en-Josas
Period15/12/0418/12/04

Cite this