A note on intersection types
Christian Retoré · 1994
: Following J.-L. Krivine, we call D the type inference system introduced by M. Coppo and M. Dezani where types are propositional formulae written with conjunction and implication from propositional letters --- there is no special constant !. We show here that the well-known result on D, stating that any term which possesses a type in D strongly normalises does not need a new reducibility argument, but is a mere consequence of strong normalization for natural deduction restricted to the conjunction and implication. The proof of strong normalization for natural deduction, and therefore our result, as opposed to reducibility arguments, can be carried out within primitive recursive arithmetic. On the other hand, this enlightens the relation between & and & that G. Pottinger has already wondered about, and can be applied to other situations, like the lambda calculus with multiplicities of G. Boudol. Key-words: Lambda calculus , intersection types , strong normalization. Logic, proof th...