Short proofs of strong normalization
Aleksander Wojdyga
TL;DR
This paper introduces straightforward syntactic proofs of strong normalization for the simply-typed and polymorphic lambda-calculi, utilizing translations to systems with established normalization properties.
Contribution
It provides new, simplified normalization proofs for complex lambda-calculi using translation techniques, covering all logical connectives and reductions.
Findings
Proofs cover full set of logical connectives
Applicable to all permutative reductions
Simplifies existing normalization proofs
Abstract
This paper presents simple, syntactic strong normalization proofs for the simply-typed lambda-calculus and the polymorphic lambda-calculus (system F) with the full set of logical connectives, and all the permutative reductions. The normalization proofs use translations of terms and types to systems, for which strong normalization property is known.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification