Geodesic
Elementary Proof of Strong Normalization for Atomic F
Bulletin of the Section of Logic, Tome 45 (2016) no. 1 Cet article a éte moissonné depuis la source Library of Science

Voir la notice de l'article

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},
     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
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/