Intersection logic

Abstract

The intersection type assignment system IT uses the formulas of the negative fragment of the predicate calculus (LJ) as types for the λ-terms. However, the deductions of IT only correspond to the proper sub-set of the derivations of LJ, obtained by imposinga metatheoretic condition about the use of the conjunction of LJ. This paper proposes a logical foundation for IT. This is done by introducing a logic IL. Intuitively, a derivation of IL is a set of derivations in LJ such that the derivations in the set can be thought of as writable in parallel. This way of lookingat LJ, by means of IL, allows to transform the metatheoretic condition, mentioned above, into a purely structural property of IL. The relation between IL and LJ surely has a first main benefit: the strongnormalization of LJ directly implies the same property on IL, which translates in a very simple proof of the strongnormalizabilit y of the λ-terms typable with IT. © Springer-Verlag Berlin Heidelberg 2001.