A note on intersection types

Christian Retoré 1
1 MEIJE - Concurrency, Synchronization and Real-time Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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 $\omega$. We show here that the well-known result on $\cal D$, stating that any term which possesses a type in $\cal D$ strongly normalises does not need a new reducibility argument, but is a mere consequence of strong normalisation for natural deduction restricted to the conjunction and implication. The proof of strong normalisation 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 enlighten the relation between $&$ and $\hat&$ that G.~Pottinger has already wondered about, and can be applied to other situations, like the lambda calculus with multiplicities of G.~Boudol.
Type de document :
RR-2431, INRIA. 1994
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:50:58
Dernière modification le : jeudi 8 novembre 2018 - 11:48:02
Document(s) archivé(s) le : lundi 5 avril 2010 - 00:07:10



  • HAL Id : inria-00074244, version 1



Christian Retoré. A note on intersection types. RR-2431, INRIA. 1994. 〈inria-00074244〉



Consultations de la notice


Téléchargements de fichiers