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 imposing a meta-theoretic 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 looking at LJ, by means of IL, allows to transform the meta-theoretic condition, mentioned above, into a purely structural property of IL. The relation between IL and LJ surely has a first main benefit: the strong normalization of LJ directly implies the same property on IL, which translates in a very simple proof of the strong normalizability of the λ-terms typable with IT.
展开▼
