Publications de l'Institut Mathematique 2007 Issue 96, Pages: 85-91
doi:10.2298/PIM0796085G
Full text ( 105 KB)


Intersection types for λGtz-calculus

Ghilezan Silvia, Ivetić Jelena

We introduce an intersection type assignment system for Espirito-Santo’s λ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.

More data about this article available through SCIndeks