Abstract FR:

Le lambda-calcul pur a ete invente vers 1930, et a connu un developpement considerable pour ses rapports etroits avec les langages de programmation fonctionnelle. Le lambda-calcul type suscite actuellement un grand interet, a cause du lien qu'il etablit entre les notions de programme et de preuve en logique intuitionniste: c'est ce qu'on appelle la correspondance de curry-howard. Parmi les systemes de typage qui ont un grand pouvoir d'expression, on trouve le systeme f des types du second ordre de girard, ainsi qu'une extension notee af2 de krivine, et le systeme ttr des types recursifs de parigot. L'interet de ces systemes est que les programmes qu'ils donnent sont prouves. Krivine a introduit en 1989 la notion d'operateurs de mise en memoire pour simuler l'appel par valeur dans le cadre d'un appel par nom. En lambda-calcul, la strategie de reduction gauche (appel par nom) a de bonnes proprietes: elle termine toujours si on l'applique a un terme normalisable; mais avec cette strategie l'argument d'une fonction est recalcule a chaque utilisation. La notion d'operateurs de mise en memoire permet de remedier a ce defaut, krivine a montre qu'en utilisant la traduction de godel de la logique classique en logique intuitionniste, on peut trouver, pour chaque type de donnees, un type tres simple pour les operateurs de mise en memoire. Ceci donne un moyen d'obtenir ces operateurs. Nous etudions dans ce travail quelques proprietes des operateurs de mise en memoire en lambda-calcul pur et type. Apres avoir expose, dans le chapitre 1, la definition des operateurs de mise en memoire, et donner les formes generales de leurs formes normales de tete; nous introduisons, dans le chapitre 2, le lambda-calcul dirige (lambda-calcul a trous diriges), outil important pour l'etude de ces operateurs, et nous prouvons que ce lambda-calcul garde les principales proprietes du lambda-calcul ordinaire. Dans le chapitre 3, nous faisons apparaitre les premieres proprietes des operateurs de mise en memoire: la stabilite de l'ensemble des operateurs de mise en memoire par la beta-equivalence, l'existence d'operateurs pour les ensembles finis de termes normaux clos, et une inegalite controlant le temps calcul d'un operateur. Le chapitre 4 expose trois sortes de types de donnees (iteratifs, descendants et recursifs), et la caracterisation des objets qu'ils contiennent. Nous y generalisons le theoreme de krivine pour des traductions de godel plus sophistiquees. Dans les chapitres 5 et 6, nous etudions les operateurs forts de mise en memoire (ceux qui donnent la forme normale), et les operateurs propres de mise en memoire (ceux qui donnent un terme clos), et nous donnons des conditions necessaires et suffisantes pour que les representations recursives et iteratives des donnees en lambda-calcul possedent des operateurs forts, et une condition suffisante pour obtenir des operateurs propres. Les chapitres 7 et 8 contiennent les resultats fondamentaux. Apres avoir defini la notion de type pour tout-positif (tous les quantificateurs du second ordre sont en position positive dans ce type), et la notion de transformation de godel (une generalisation de la traduction de godel classique) du systeme af2 et ttr; nous generalisons, en utilisant des methodes purement syntaxiques, le theoreme de krivine sur ces types et pour ces transformations