The "Relevance" of Intersection and Union Types
Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Betti Venneri · Notre Dame Journal of Formal Logic · 1997
The aim of this paper is to investigate a Curry-Howard interpretation of the intersection and union type inference system for Combinatory Logic. Types are interpreted as formulas of a Hilbert-style logic L, which turns out to be an extension of the intuitionistic logic with respect to provable disjunctive formulas (because of new equivalence relations on formulas), while the implicational-conjunctive fragment of L is still a fragment of intuitionistic logic. Moreover, typable terms are translated in a typed version, so that $\vee$-$\wedge$-typed combinatory logic terms are proved to completely codify the associated logical proofs.