A formalization of Γ in Coq

By Robbert Krebbers as part of a research project of the “Foundations” master program at the Radboud University. Supervised by James McKinna

Paper Abstract

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.

Download paper and Coq sources