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 
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/
@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},
     year = {2016},
     volume = {45},
     number = {1},
     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
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
%U http://geodesic.mathdoc.fr/item/BSL_2016_45_1_a3/
%G en
%F BSL_2016_45_1_a3