Abstract

This paper presents a notion of intersection and union type assignment for the calculus X, a substitution free language that can be used to describe the behaviour of functional programming languages at a very low level of granularity, and has first been defined in \cite{Lengrand'03,vBLL'04}. X has been designed to give a Curry-Howard-de Bruijn correspondence to the sequent calculus for classical logic. In this paper we will define a notion of sequent-style intersection type assignment on X that needs union types, and show that this notion is closed for both subject-reduction and subject-expansion. We will also show that it is an extension of the Strict system for the Lambda Calculus.

Appeared as:

@Inproceedings{Bakel-ITRS'04,

Author = "S. van Bakel",
Title = "{I}ntersection and {U}nion {T}ypes for $\cal X$",
Booktitle = "Electronic Proceedings of International Workshop {\em Intersection Types and Related Systems 2002} (ITRS'04), Turku, Finland",
Series = "Electronic Notes in Theoretical Computer Science",
Year = "2004"
}