Publications de l'Institut Mathématique, Nouvelle SérieVol. 82(96), pp. 85–91 (2007)
|
|
Publications de l'Institut Mathématique, Nouvelle Série Vol. 82(96), pp. 85–91 (2007) |
|
|
INTERSECTION TYPES FOR $\lambda^{\mathsf{Gtz}}$-CALCULUSS. Ghilezan and J. IveticTehnicki fakultet, 21000 Novi Sad, SerbiaAbstract: 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
|