A Machine-checked Proof of Consistency for Impredicative Pure Type Systems
arXiv:2607.20188 · doi:10.4204/EPTCS.449.15
Abstract
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 some substantial progress. We present formal proofs of confluence for beta-reduction and by using Takahashi's revision of Tait and Martin-Löf's proof, subject reduction for the entire family of the Pure Type Systems and consistency for some impredicative subclass, assuming normalization. As to the proof of confluence, we also develop a theory of alpha-commutative relations which, in our view, entails a clearer presentation and treatment of the problem than in similar developments. Finally, we assess general merits and drawbacks of the approach. The whole development has been machine-checked using Agda.
In Proceedings LSFA 2026, arXiv:2607.15904
References in corpus (3)
- Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution
- A Formal Proof of the Strong Normalization Theorem for System T in Agda
- On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions