Geodesic
Intersection Types for lambda^{gtz}-calculus
Publications de l'Institut Mathématique, _N_S_82 (2007) no. 96, p. 85 .

Voir la notice de l'article provenant de la source eLibrary of Mathematical Institute of the Serbian Academy of Sciences and Arts

We introduce an intersection type assignment system for the Espirito-Santo's $\lambda^{\mathsf{Gtz}}$-calculus, a term calculus embodying the Curry--Howard correspondence for the intuitionistic sequent calculus. We investigate basic properties of this intersection type system. Our main result is Subject reduction property.
DOI : 10.2298/PIM0796085G
Classification : 03B40 68N18 
@article{10_2298_PIM0796085G,
     author = {Silvia Ghilezan and J. Iveti\'c},
     title = {Intersection {Types} for lambda^{gtz}-calculus},
     journal = {Publications de l'Institut Math\'ematique},
     pages = {85 },
     publisher = {mathdoc},
     volume = {_N_S_82},
     number = {96},
     year = {2007},
     doi = {10.2298/PIM0796085G},
     zbl = {1164.03001},
     language = {en},
     url = {http://geodesic.mathdoc.fr/articles/10.2298/PIM0796085G/}
}
TY  - JOUR
AU  - Silvia Ghilezan
AU  - J. Ivetić
TI  - Intersection Types for lambda^{gtz}-calculus
JO  - Publications de l'Institut Mathématique
PY  - 2007
SP  - 85 
VL  - _N_S_82
IS  - 96
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/articles/10.2298/PIM0796085G/
DO  - 10.2298/PIM0796085G
LA  - en
ID  - 10_2298_PIM0796085G
ER  - 
%0 Journal Article
%A Silvia Ghilezan
%A J. Ivetić
%T Intersection Types for lambda^{gtz}-calculus
%J Publications de l'Institut Mathématique
%D 2007
%P 85 
%V _N_S_82
%N 96
%I mathdoc
%U http://geodesic.mathdoc.fr/articles/10.2298/PIM0796085G/
%R 10.2298/PIM0796085G
%G en
%F 10_2298_PIM0796085G
Silvia Ghilezan; J. Ivetić. Intersection Types for lambda^{gtz}-calculus. Publications de l'Institut Mathématique, _N_S_82 (2007) no. 96, p. 85 . doi : 10.2298/PIM0796085G. http://geodesic.mathdoc.fr/articles/10.2298/PIM0796085G/

Cité par Sources :