Publications de l'Institut Mathematique 2007 Issue 96, Pages: 85-91
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