Les I-types du système
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 35 (2001) no. 3, pp. 223-237.

Nous démontrons dans ce papier que les types du système habités uniquement par des λI-termes (les I-types) sont à quantificateur positif. Nous présentons ensuite des conséquenses de ce résultat et quelques exemples.

We prove in this paper that the types of system inhabited uniquely by λI-terms (the I-types) have a positive quantifier. We give also consequences of this result and some examples.

Classification : 03B40,  68Q60
Mots clés : λI-calculus, system , I-type
@article{ITA_2001__35_3_223_0,
     author = {Nour, K.},
     title = {Les $I$-types du syst\`eme $\mathcal {F}$},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {223--237},
     publisher = {EDP-Sciences},
     volume = {35},
     number = {3},
     year = {2001},
     zbl = {0991.03021},
     mrnumber = {1869215},
     language = {fr},
     url = {http://www.numdam.org/item/ITA_2001__35_3_223_0/}
}
TY  - JOUR
AU  - Nour, K.
TI  - Les $I$-types du système $\mathcal {F}$
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2001
DA  - 2001///
SP  - 223
EP  - 237
VL  - 35
IS  - 3
PB  - EDP-Sciences
UR  - http://www.numdam.org/item/ITA_2001__35_3_223_0/
UR  - https://zbmath.org/?q=an%3A0991.03021
UR  - https://www.ams.org/mathscinet-getitem?mr=1869215
LA  - fr
ID  - ITA_2001__35_3_223_0
ER  - 
Nour, K. Les $I$-types du système $\mathcal {F}$. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 35 (2001) no. 3, pp. 223-237. http://www.numdam.org/item/ITA_2001__35_3_223_0/

[1] H. Barendregt, The lambda calculus, its syntax and semantics. North Holland (1984). | MR 774952 | Zbl 0551.03007

[2] S. Farkh, Types de données en logique du second ordre, Thèse de doctorat. Université de Savoie, France (1998).

[3] J.-Y. Girard, Y. Lafont et P. Taylor, Proofs and types. Cambridge University Press (1986). | MR 1003608 | Zbl 0671.68002

[4] J.-L. Krivine, Lambda calcul, types et modèles. Masson (1990). | MR 1162977 | Zbl 0697.03004

[5] K. Nour, Opérateurs de mise en mémoire et types -positifs. RAIRO : Theoret. Informatics Appl. 30 (1996) 261-293. | EuDML 92537 | Numdam | MR 1415831 | Zbl 0869.03009