Intersection and Union Types for X

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 [12,5]. 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 lc