Short proofs of strong normalization

Preprint English OPEN
Wojdyga, Aleksander (2008)
  • Subject: Computer Science - Logic in Computer Science | F.4.1
    arxiv: Computer Science::Logic in Computer Science

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.
  • References (10)

    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.

    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.

    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.

  • Metrics
    No metrics available
Share - Bookmark