Intersection Types for lambda^{Gtz}-calculus


S. Ghilezan, J. Ivetić


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.