A binary modal logic for the intersection types of lambda-calculus

Intersection types discipline allows to define a wide variety of models for the type free lambda-calculus, but the Curry-Howard isomorphism breaks down for this kind of type systems. In this paper we show that the correspondence between types and suitable logical formulas can still be recovered appealing to the fact that there is a strict connection between the semantics for lambda-calculus induced by the intersection types and a Kripke-style semantics for modal and relevant logics. Indeed, we present a modal logic hinted by the analysis of the sub-typing relation for intersection types, and we show that the deduction relation for such a modal system is a conservative extension of the relation of sub-typing. Then, we define a Kripke-style semantics for the formulas of such a system, present suitable sequential calculi, prove a completeness theorem and give a syntactical proof of the cut elimination property. Finally, we define a decision procedure for theorem-hood and we show that it yields the finite model property and cut-redundancy.