Pure type systems without explicit contexts

J.H. Geuvers, R. Krebbers, J. McKinna, F. Wiedijk

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Citations (Scopus)

Abstract

We present an approach to type theory in which the typing judgments do not have explicit contexts. Instead of judgments of shape "Gamma |- A : B", our systems just have judgments of shape "A : B". A key feature is that we distinguish free and bound variables even in pseudo-terms. Specifically we give the rules of the "Pure Type System" class of type theories in this style. We prove that the typing judgments of these systems correspond in a natural way with those of Pure Type Systems as traditionally formulated. I.e., our systems have exactly the same well-typed terms as traditional presentations of type theory. Our system can be seen as a type theory in which all type judgments share an identical, infinite, typing context that has infinitely many variables for each possible type. For this reason we call our system "Gamma_infinity". This name means to suggest that our type judgment "A : B" should be read as "Gamma_infinity |- A : B", with a fixed infinite type context called "Gamma_infinity".
Original languageEnglish
Title of host publicationProceedings of the 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2010, Edinburgh, UK, July 14, 2010)
EditorsK. Crary, M. Miculan
PublisherEPTCS
Pages53-67
DOIs
Publication statusPublished - 2010

Publication series

NameElectronic Proceedings in Theoretical Computer Science
Volume34
ISSN (Print)2075-2180

Fingerprint Dive into the research topics of 'Pure type systems without explicit contexts'. Together they form a unique fingerprint.

Cite this