@inproceedings{b301490f0f704686b2a0dcd619cef525,

title = "Pure type systems without explicit contexts",

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{"}.",

author = "J.H. Geuvers and R. Krebbers and J. McKinna and F. Wiedijk",

year = "2010",

doi = "10.4204/EPTCS.34.6",

language = "English",

series = "Electronic Proceedings in Theoretical Computer Science",

publisher = "EPTCS",

pages = "53--67",

editor = "K. Crary and M. Miculan",

booktitle = "Proceedings of the 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2010, Edinburgh, UK, July 14, 2010)",

}