# A note on intersection types

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.
Keywords :
Type de document :
Rapport
RR-2431, INRIA. 1994
Domaine :

Littérature citée [18 références]

https://hal.inria.fr/inria-00074244
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:50:58
Dernière modification le : samedi 27 janvier 2018 - 01:31:03
Document(s) archivé(s) le : lundi 5 avril 2010 - 00:07:10

### Identifiants

• HAL Id : inria-00074244, version 1

### Citation

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

### Métriques

Consultations de la notice

## 123

Téléchargements de fichiers