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.