publication . Part of book or chapter of book . Preprint . 2008

Short Proofs of Strong Normalization

Aleksander Wojdyga;
Open Access
  • Published: 16 Apr 2008
  • Publisher: Springer Berlin Heidelberg
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.
Persistent Identifiers
arXiv: Computer Science::Logic in Computer Science
free text keywords: Computer Science - Logic in Computer Science, F.4.1, Normalization (statistics), Syntax, Lambda calculus, computer.programming_language, computer, System F, Mathematics, Mathematical proof, Discrete mathematics, Logical connective
Download fromView all 2 versions
Part of book or chapter of book
Provider: UnpayWall
Part of book or chapter of book . 2008
Provider: Crossref

1. R. David and K. Nour. A short proof of the strong normalization of classical natural deduction with disjunction. Journal of Symbolic Logic, 68(4):1277-1288, 2003. [OpenAIRE]

2. Ph. de Groote. On the strong normalisation of natural deduction with permutationconversions. In P. Narendran and M. Rusinowitch, editors, Proceedings 10th Int. Conf. on Rewriting Techniques and Applications, RTA'99, Trento, Italy, 2-4 July 1999, volume 1631 of Lecture Notes in Computer Science, pages 45-59. Berlin, 1999.

3. Ph. de Groote. On the strong normalisation of intuitionistic natural deduction with permutation-conversions. Information and Computation, 178(2):441-464, 2002.

4. J.-Y. Girard. The Blind Spot. Lectures on Logic. Rome, Autumn 2004. girard/coursang/coursang.html.

5. F. Joachimski and R. Matthes. Short proofs of normalization for the simplytyped λ-calculus, permutative conversions and G¨odel's T. Archive for Mathematical Logic, 42(1):59-87, 2003.

6. M. Tatsuta K. Nakazawa. Strong normalization of classical natural deduction with disjunctions. Annals of Pure and Applied Logic, doi:10.1016/j.apal.2008.01.003, 2008.

7. H. Schwichtenberg. Minimal logic for computable functionals. In Logic Colloquium 2005. A.K. Peters. To appear.

8. M.H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006.

9. M. Tatsuta. Second-order permutative conversions with Prawitz's strong validity. Progresss in Informatics, 2:41-56, 2005. [OpenAIRE]

10. M. Tatsuta. Simple saturated sets for disjunction and second-order existential quantification. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications, volume 4583 of Lecture Notes in Computer Science, pages 366-380. Springer, 2007.

Any information missing or wrong?Report an Issue