Pure Type Systems without Explicit Contexts
Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk, K. Crary, Miculan M. · 2009
Abstract. 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 Γ∞.