Elementary Proof of Strong Normalization for Atomic F

&
Bulletin of the Section of Logic 45 (1):1-15 (2016)
  Copy   BIBTEX

Abstract

We give an elementary proof of the strong normalization of the atomic polymorphic calculus Fat.

Categories

Add categories

Keywords

Reprint years

DOI

10.18778/0138-0680.45.1.01

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,503

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

η- conversions of IPC implemented in atomic F.Gilda Ferreira - 2017 - Logic Journal of the IGPL 25 (2):115-130.
Atomic polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.
The Faithfulness of Fat: A Proof-Theoretic Proof.Fernando Ferreira & Gilda Ferreira - 2015 - Studia Logica 103 (6):1303-1311.
A Short Proof Of The Strong Normalization Of Classical Natural Deduction With Disjunction.René David & Karim Nour - 2003 - Journal of Symbolic Logic 68 (4):1277-1288.
A short proof of the strong normalization of classical natural deduction with disjunction.René David & Karim Nour - 2003 - Journal of Symbolic Logic 68 (4):1277-1288.
A simple proof of second-order strong normalization with permutative conversions.Makoto Tatsuta & Grigori Mints - 2005 - Annals of Pure and Applied Logic 136 (1-2):134-155.
An elementary proof of strong normalization for intersection types.Valentini Silvio - 2001 - Archive for Mathematical Logic 40 (7):475-488.
Strong Normalization via Natural Ordinal.Daniel Durante Pereira Alves - 1999 - Dissertation,
Some general results about proof normalization.Marc Aiguier & Delphine Longuet - 2010 - Logica Universalis 4 (1):1-29.
Strong normalization proof with CPS-translation for second order classical natural deduction.Koji Nakazawa & Makoto Tatsuta - 2003 - Journal of Symbolic Logic 68 (3):851-859.
Corrigendum to “Strong normalization proof with CPS-translation for second order classical natural deduction”.Koji Nakazawa & Makoto Tatsuta - 2003 - Journal of Symbolic Logic 68 (4):1415-1416.
A reduction rule for Peirce formula.Sachio Hirokawa, Yuichi Komori & Izumi Takeuti - 1996 - Studia Logica 56 (3):419 - 426.
A semantical proof of the strong normalization theorem for full propositional classical natural deduction.Karim Nour & Khelifa Saber - 2006 - Archive for Mathematical Logic 45 (3):357-364.
A formalization of Sambins's normalization for GL.Edward Hermann Haeusler & Luiz Carlos Pereira - 1993 - Mathematical Logic Quarterly 39 (1):133-142.
A Formalization Of Sambins's Normalization For Gl.Edward Hauesler & Luiz Carlos Pereira - 1993 - Mathematical Logic Quarterly 39 (1):133-142.

Analytics

Added to PP
2019-06-09

Downloads
14 (#982,380)

6 months
2 (#1,194,813)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

η- conversions of IPC implemented in atomic F.Gilda Ferreira - 2017 - Logic Journal of the IGPL 25 (2):115-130.

Add more citations

References found in this work

Intensional interpretations of functionals of finite type I.W. W. Tait - 1967 - Journal of Symbolic Logic 32 (2):198-212.
Exact Bounds for lengths of reductions in typed λ-calculus.Arnold Beckmann - 2001 - Journal of Symbolic Logic 66 (3):1277-1285.
An upper bound for reduction sequences in the typed λ-calculus.Helmut Schwichtenberg - 1991 - Archive for Mathematical Logic 30 (5-6):405-408.
A Simple Proof of Parsons' Theorem.Fernando Ferreira - 2005 - Notre Dame Journal of Formal Logic 46 (1):83-91.

Add more references