A Formal Proof of the Strong Normalization Theorem for System T in Agda

DOI10.4204/eptcs.376.8arXiv2303.13258WikidataQ122402818 ScholiaQ122402818MaRDI QIDQ6118750

Sebastián Urciuoli

Publication date: 28 February 2024

Published in: Electronic Proceedings in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2303.13258

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Cites Work

• Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
• Substitution revisited
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Nominal unification
• The locally nameless representation
• Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda
• Formal metatheory of the lambda calculus using Stoughton's substitution
• Normalization for the Simply-Typed Lambda-Calculus in Twelf
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• POPLMark reloaded: Mechanizing proofs by logical relations
• Intensional interpretations of functionals of finite type I
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item