Wojdyga, Aleksander 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]. Cited in 2 Documents MSC: 03B40 Combinatory logic and lambda calculus 03F05 Cut-elimination and normal-form theorems 03F20 Complexity of proofs Keywords:strong normalization; CPS-translation; permutative reductions; lambda calculus; System F PDFBibTeX XMLCite \textit{A. Wojdyga}, Lect. Notes Comput. Sci. 5162, 613--623 (2008; Zbl 1173.03303) Full Text: DOI arXiv