Elementary Proof of Strong Normalization for Atomic F
Fernando Ferreira; Gilda Ferreira
Bulletin of the Section of Logic (2016)
- Volume: 45, Issue: 1
- ISSN: 0138-0680
Access Full Article
top
Abstract
topHow to cite
topFernando Ferreira, and Gilda Ferreira. "Elementary Proof of Strong Normalization for Atomic F." Bulletin of the Section of Logic 45.1 (2016): null. <http://eudml.org/doc/295571>.
@article{FernandoFerreira2016,
abstract = {We give an elementary proof (in the sense that it is formalizable in Peano arithmetic) of the strong normalization of the atomic polymorphic calculus Fat (a predicative restriction of Girard’s system F).},
author = {Fernando Ferreira, Gilda Ferreira},
journal = {Bulletin of the Section of Logic},
keywords = {Predicative polymorphism; strong normalization; elementary proofs; lambda-calculus},
language = {eng},
number = {1},
pages = {null},
title = {Elementary Proof of Strong Normalization for Atomic F},
url = {http://eudml.org/doc/295571},
volume = {45},
year = {2016},
}
TY - JOUR
AU - Fernando Ferreira
AU - Gilda Ferreira
TI - Elementary Proof of Strong Normalization for Atomic F
JO - Bulletin of the Section of Logic
PY - 2016
VL - 45
IS - 1
SP - null
AB - We give an elementary proof (in the sense that it is formalizable in Peano arithmetic) of the strong normalization of the atomic polymorphic calculus Fat (a predicative restriction of Girard’s system F).
LA - eng
KW - Predicative polymorphism; strong normalization; elementary proofs; lambda-calculus
UR - http://eudml.org/doc/295571
ER -
References
top- [1] T. Altenkirch and T. Coquand, A finitary subsystem of the polymorphic λ-calculus, Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications (TLCA 2001), Lecture Notes in Computer Science 2044 (2001), pp. 22–28.
- A. Beckmann, Exact bounds for lenghts of reductions in typed λ-calculus, The Journal of Symbolic Logic 66(3) (2001), pp. 1277–1285.
- F. Ferreira, A simple proof of Parsons’ theorem, Notre Dame Journal of Formal Logic 46 (2005), pp. 83–91.
- F. Ferreira, Comments on predicative logic, Journal of Philosophical Logic 35 (2006), pp. 1–8.
- F. Ferreira and G. Ferreira, Atomic polymorphism, The Journal of Symbolic Logic 78 (2013), pp. 260–274.
- F. Ferreira and G. Ferreira, The faithfulness of Fat : a proof-theoretic proof, Studia Logica 103(6) (2015), pp. 1303–1311.
- J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and Types, Cambridge University Press (1989).
- F. Joachimski and R. Matthes, Short proofs of normalization for the simplytyped lambda-calculus, permutative conversions and Gödel’s T, Archive for Mathematical Logic 42 (2003), pp. 59–87.
- H. Schwichtenberg, An upper bound for reduction sequences in the typed λ-calculus, Archive for Mathematical Logic 30 (1991), pp. 405–408.
- W. Tait, Intentional interpretations of functionals of finite type I, The Journal of Symbolic Logic 32 (1967), pp. 198–212.
- W. Tait, Finitism, Journal of Philosophy 78 (1981), pp. 524–546.
- A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, Cambridge University Press (1996).
- A. S. Troelstra and D. van Dalen, Constructivism in Mathematics. An Introduction, volume 1, North Holland, Amsterdam (1988).
- J. van de Pol, Two different strong normalization proofs? Computability versus functionals of finite type, Proceedings of the Second International Workshop on Higher-Order Algebra, Logic and Term Rewriting (HOA’95), Lecture Notes in Computer Science 1074 (1996), pp. 201–220.
- F. van Raamsdonk and P. Severi, On normalization, Technical report CSR9545, Centrum voor Wiskunde en Informatica, Amsterdam (1995).
NotesEmbed ?
topYou must be logged in to post comments.
To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.