Geodesic
Intersection Types for lambda^{gtz}-calculus
Publications de l'Institut Mathématique, _N_S_82 (2007) no. 96, p. 85 Cet article a éte moissonné depuis la source eLibrary of Mathematical Institute of the Serbian Academy of Sciences and Arts

Voir la notice de l'article

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 },
     year = {2007},
     volume = {_N_S_82},
     number = {96},
     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
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
%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

Cité par Sources :