Pure Type Systems without Explicit Contexts

Herman Geuvers
(Radboud University Nijmegen)
Robbert Krebbers
(Radboud University Nijmegen)
James McKinna
(Radboud University Nijmegen)
Freek Wiedijk
(Radboud University Nijmegen)

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

In Karl Crary and Marino Miculan: Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2010), Edinburgh, UK, 14th July 2010, Electronic Proceedings in Theoretical Computer Science 34, pp. 53–67.
Published: 11th September 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.34.6 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org