Pure Type Systems without Explicit Contexts

Herman Geuvers, Robbert Krebbers, James McKinna +1

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 o…