Abstract

This paper studies intersection and union type assignment for the calculus , a proof-term syntax for Gentzen’s classical sequent calculus, with the aim of defining a type-based semantics, via setting up a system that is closed under conversion. We will start by investigating what the minimal requirements are for a system, for to be complete ; this coincides with System , the notion defined in Dougherty et al. [18]; however, we show that this system is not sound , so our goal cannot be achieved. We will then show that System is also not complete, but can recover from this by presenting System as an extension of and showing that it satisfies completeness; it still lacks soundness. We show how to restrict so that it satisfies soundness as well by limiting the applicability of certain type assignment rules, but only when limiting reduction to call-by-name or call-by-value reduction; in restricting the system this way, we sacrifice completeness. These results when combined show that, with respect to full reduction, it is not possible to define a sound and complete intersection and union type assignment system for