By Robbert Krebbers as part of a research project of the “Foundations” master program at the Radboud University. Supervised by James McKinna
In this paper we present a formalization of the type systems Γ∞ in the proof assistant Coq. The family of type systems Γ∞, described in a recent article by Geuvers, McKinna and Wiedijk, presents type theory without the need for explicit contexts. A typing judgment in Γ∞ is of the shape A :∞ B while an ordinary judgment is of the shape Γ ⊢ A : B.
This approach of Geuvers et al. makes a bridge between traditional logic and type theory. In the former free variables are really free and contexts are non-explicit, as in Γ∞ . Furthermore Γ∞ could make it possible to create a stateless version of an LCF style prover.
The important part of the work of Geuvers et al. is a theorem that states that there is a natural correspondence between judgments in Γ∞ and ordinary Pure Type Systems. Their paper contains an informal proof of this theorem. We have formalized many of their definitions and lemmas which results in a proof of one direction of this correspondence theorem.