Intersection and union types_ Syntax and semantics

authors: F Barbanera, M Dezaniciancaglini, U Deliguoro
year: 1995
url: https://linkinghub.elsevier.com/retrieve/pii/S0890540185710863
publisher: Elsevier BV
abstract: Type assignment systems with intersection and union types are introduced. Although the subject reduction property with respect to ?-reduction does not hold for a natural deduction-like system, we manage to overcome this problem in two, different ways. The first is to adopt a notion of parallel reduction, which is a refinement of Gross-Knuth reduction. The second is to introduce type theories to refine the system, among which is the theory called ? that induces an assignment system preserving ?-reduction. This type assignment system further clarifies the relation with the intersection discipline through the decomposition, first, of a disjunctive type into a set of conjunctive types and, second, of a derivation in the new type assignment system into a set of derivations in the intersection type assignment system. For this system we propose three semantics and prove soundness and completeness theorems.