×

Short proofs of strong normalization. (English) Zbl 1173.03303

Ochmański, Edward (ed.) et al., Mathematical foundations of computer science 2008. 33rd international symposium, MFCS 2008, Toruń Poland, August 25–29, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-85237-7/pbk). Lecture Notes in Computer Science 5162, 613-623 (2008).
Summary: This paper presents simple, syntactic strong normalization proofs for the simply-typed \(\lambda \)-calculus and the polymorphic \(\lambda \)-calculus (System \(\mathbf {F}\)) with the full set of logical connectives, and all the permutative reductions. The normalization proofs use translations of terms and types of \(\lambda_{\to, \land, \lor, \perp}\) to terms and types of \(\lambda_{\to}\) and from \(\mathbf {F}_{\forall, \exists, \to, \land, \lor, \perp}\) to \(\mathbf {F}_{\forall, \to}\).
For the entire collection see [Zbl 1154.68021].

MSC:

03B40 Combinatory logic and lambda calculus
03F05 Cut-elimination and normal-form theorems
03F20 Complexity of proofs
PDFBibTeX XMLCite
Full Text: DOI arXiv