A Machine-checked Proof of Consistency for Impredicative Pure Type Systems

Sebastián Urciuoli

In this paper we continue assessing the feasibility of the approach to the mechanization of type theory by using classical syntax and Stoughton's multiple substitutions and report…