Les I-types du système ℱ
Nour, K.
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 35 (2001), p. 223-237 / Harvested from Numdam
Access to full text
Full (PDF)
Full (DJVU)

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.

Publié le : 2001-01-01
Classification:  03B40,  68Q60 
@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},
     volume = {35},
     year = {2001},
     pages = {223-237},
     mrnumber = {1869215},
     zbl = {0991.03021},
     language = {fr},
     url = {http://dml.mathdoc.fr/item/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) pp. 223-237. http://gdmltest.u-ga.fr/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. | Numdam | MR 1415831 | Zbl 0869.03009