Abstract FR:

Ce travail de thèse étudie le systeme af2 de j. L. Krivine, qui est une extension du système f de j. Y. Girard. Dans af2, on peut obtenir un programme calculant une fonction, en exprimant les types de données algébriques (booléens, entiers, liste d'entiers)et en écrivant une démonstration de la totalité de la fonction. La classe a des types de données algébriques à la particularité suivante : un terme normal est typable d'un type d. A ssi il est dans l'interprétation de d, pour la sémantique de réalisabilité. Le but était de construire des classes (selon la sémantique adaptée des parties saturées) plus larges de types ayant cette particularité. Ces types nous les avons appelés types complets, puisque la sémantique considérée est complète pour ces types. Nous avons montré que les types a quantificateurs positifs (les quantifications du second ordre n'apparaissent pas en position negative) dans af2 sont des types complets pour la sémantique des parties saturées par -équivalence. Comme on avait besoin dans la démonstration de la conservation de type par -réduction (en effet, le système af2 n'a pas cette propriété) et comme la clôture par expansion faible de tête est une notion plus faible que celle de clôture par -équivalence, on était intéressé à étendre ce résultat a un modèle sature par expansion faible de tête. Ceci nous a amené à construire une classe plus restreinte de types (les bons types positifs), pour lesquels la -réduction est préservée et qui sont complets pour la sémantique des parties saturées par expansion faible de tête. Une deuxième façon pour avoir la préservation de types par -réduction était d'étendre af2 a un système de typage af2s qui a seulement trois règles de typage et parametre par une relation de sous typage. Nous avons montré que af2s n'est autre que af2 auquel on ajoute la préservation de type par -réduction comme règle de typage. Ensuite nous avons montré dans af2s, que les types a quantificateurs positifs sont complets pour la sémantique des parties stables par expansion faible de tête. Dans le dernier chapitre on a donné une définition d'un type de données du système f par des types entree-sortie qui servent à caractériser les domaines et codomaines des fonctions que l'on cherche à programmer. Nous avons montre que les types à quantificateurs positifs sont des types entrée et sortie, que tout type entrée est un type sortie. La réciproque est démontrée dans des cas particuliers, ou on impose des restrictions sur la règle d'élimination des quantificateurs du second ordre. La thèse conclut avec d'autres résultats, en particulier sur les opérateurs de mise en mémoire de j. L. Krivine.