Short proofs of strong normalization

Preprint English OPEN
Wojdyga, Aleksander;
(2008)
  • Subject: Computer Science - Logic in Computer Science | F.4.1
    acm: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES | TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
    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 ... View more
  • 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. http://iml.univ-mrs.fr/ 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
Share - Bookmark