Completeness and partial soundness results for intersection and union typing for

This paper studies intersection and union type assignment for the calculus (Curien and Herbelin, 2000 [16]), 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 (closed under redex expansion); this coincides with System M∩∪, the notion defined in Dougherty et al. (2004) [18]; however, we show that this system is not sound (closed under subject reduction), so our goal cannot be achieved. We will then show that System M∩∪ is also not complete, but can recover from this by presenting System as an extension of M∩∪ (by adding typing rules) and showing that it satisfies completeness; it still lacks soundness. We show how to restrict M∩∪ so that it satisfies soundness as well by limiting the applicability of certain type assignment rules, but only when limiting reduction to (confluent) 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 .