Geodesic
Elementary Proof of Strong Normalization for Atomic F
Bulletin of the Section of Logic, Tome 45 (2016) no. 1.

Voir la notice de l'article provenant de la source Library of Science

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).
Keywords: Predicative polymorphism, strong normalization, elementary proofs, lambda-calculus 
@article{BSL_2016_45_1_a3,
     author = {Ferreira, Fernando and Ferreira, Gilda},
     title = {Elementary {Proof} of {Strong} {Normalization} for {Atomic} {F}},
     journal = {Bulletin of the Section of Logic},
     publisher = {mathdoc},
     volume = {45},
     number = {1},
     year = {2016},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2016_45_1_a3/}
}
TY  - JOUR
AU  - Ferreira, Fernando
AU  - Ferreira, Gilda
TI  - Elementary Proof of Strong Normalization for Atomic F
JO  - Bulletin of the Section of Logic
PY  - 2016
VL  - 45
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2016_45_1_a3/
LA  - en
ID  - BSL_2016_45_1_a3
ER  - 
%0 Journal Article
%A Ferreira, Fernando
%A Ferreira, Gilda
%T Elementary Proof of Strong Normalization for Atomic F
%J Bulletin of the Section of Logic
%D 2016
%V 45
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2016_45_1_a3/
%G en
%F BSL_2016_45_1_a3
Ferreira, Fernando; Ferreira, Gilda. Elementary Proof of Strong Normalization for Atomic F. Bulletin of the Section of Logic, Tome 45 (2016) no. 1. http://geodesic.mathdoc.fr/item/BSL_2016_45_1_a3/