EMIS ELibM Electronic Journals Publications de l'Institut Mathématique, Nouvelle Série
Vol. 82(96), pp. 85–91 (2007)

Previous Article

Next Article

Contents of this Issue

Other Issues

ELibM Journals

ELibM Home


Pick a mirror



S. Ghilezan and J. Ivetic

Tehnicki fakultet, 21000 Novi Sad, Serbia

Abstract: 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.

Classification (MSC2000): 03B40; 68N18

Full text of the article: (for faster download, first choose a mirror)

Electronic fulltext finalized on: 20 Feb 2008. This page was last modified: 26 Feb 2008.

© 2008 Mathematical Institute of the Serbian Academy of Science and Arts
© 2008 ELibM and FIZ Karlsruhe / Zentralblatt MATH for the EMIS Electronic Edition