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 : $\lambda I$-calculus, system ${\mathcal {F}}$, $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},
     mrnumber = {1869215},
     zbl = {0991.03021},
     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
SP  - 223
EP  - 237
VL  - 35
IS  - 3
PB  - EDP-Sciences
UR  - http://www.numdam.org/item/ITA_2001__35_3_223_0/
LA  - fr
ID  - ITA_2001__35_3_223_0
ER  - 
%0 Journal Article
%A Nour, K.
%T Les $I$-types du système $\mathcal {F}$
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2001
%P 223-237
%V 35
%N 3
%I EDP-Sciences
%U http://www.numdam.org/item/ITA_2001__35_3_223_0/
%G fr
%F ITA_2001__35_3_223_0
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 | Zbl

[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 | Zbl

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

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