  The intersection type assignment system has been designed directly as
deductive system for assigning formulae of the implicative and conjunctive
fragment of the intuitionistic logic to terms of lambda-calculus. But its
relation with the logic is not standard. Between all the logics that have been
proposed as its foundation, we consider ISL, which gives a logical
interpretation of the intersection by splitting the intuitionistic conjunction
into two connectives, with a local and global behaviour respectively, being the
intersection the local one. We think ISL is a logic interesting by itself, and
in order to support this claim we give a sequent calculus formulation of it,
and we prove that it enjoys the cut elimination property.

Logic in Computer Science;Programming Languages