RAIRO - Theoretical Informatics and Applications (RAIRO: ITA)

Issue		Theoret. Informatics Appl. Volume 35, Number 3, May-June 2001
Page(s)		223 - 237
DOI		10.1051/ita:2001116

DOI: 10.1051/ita:2001116

Theoret. Informatics Appl. 35, 223-237 (2001)

LES I-TYPES DU SYSTÈME ${\cal F}$

K. Nour

LAMA, Équipe de Logique, Université de Chambéry, 73376 Le Bourget du Lac, France ; (nour@univ-savoie.fr)

(Recu le 12 avril 1999. Accepté le 30 mars 2001.)

Abstract
We prove in this paper that the types of system ${\cal F}$ inhabited uniquely by $\lambda I$ -terms (the I-types) have a positive quantifier. We give also consequences of this result and some examples.

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

AMS Subject: 03B40, 68Q60.

Key words: $\lambda I$ -calculus -- system ${\cal F}$ -- I-type.

© EDP Sciences 2001

What is OpenURL?