Reduction in X does not agree with Intersection and Union Types (Extended abstract)

TL;DR

This paper investigates the properties of intersection and union type assignments in calculus X, revealing limitations in their compatibility with standard type system properties like subject-reduction and expansion.

Contribution

It introduces intersection and union types for calculus X and analyzes their closure properties, highlighting the need for restrictions to maintain type system consistency.

Findings

Type assignment is closed under subject-expansion.

Type assignment requires restrictions to satisfy subject-reduction.

The notion is unsuitable for defining semantics due to these limitations.

Abstract

This paper defines intersection and union type assignment for the calculus X, a substitution free language that enjoys the Curry-Howard correspondence with respect to Gentzen's sequent calculus for classical logic. We show that this notion is closed for subject-expansion, and show that it needs to be restricted to satisfy subject-reduction as well, making it unsuitable to define a semantics.