Intersection Types as Logical Formulae

Abstract

The aim of this paper is to investigate, in the Curry-Howard isomorphism approach, a logical characterization for the intersection-type discipline. First a novel formulation of the intersection type inference for combinatory logic is presented, such that it is equivalent to the original version of the system, while the intersection operator is no longer dealt with as a proof-theoretical connective. Then a Hilbert-style axiomatization is defined and proved to totally parallel intersection-derivability, in such a way that inhabited intersection-types are all and only the provable formulae in the logic system.