Sciweavers

CORR
2010
Springer

Pure Type Systems without Explicit Contexts

13 years 11 months ago
Pure Type Systems without Explicit Contexts
We present an approach to type theory in which the typing judgments do not have explicit contexts. Instead of judgments of the shape A : B, our systems just have judgments of the shape A : B. An essential feature of our systems is that already in pseudo-terms we distinguish the free from the bound variables. Specifically we give the rules of the `Pure Type System' class of type theories in this style. We prove that the type judgments of these systems corresponds in a natural way with the judgments of the traditionally formulated Pure Type Systems. 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 . This name means to suggest that our type judgment A : B should be read as A : B, with a fixed infinite type context called .
Herman Geuvers, Robbert Krebbers, James McKinna, F
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2010
Where CORR
Authors Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk
Comments (0)