Autour du lambda-calcul avec constructeurs

Le lambda calcul avec constructeurs (de Arbiser, Miquel et Rios) est une extension du lambda calcul avec un mecanisme de filtrage. Le filtrage a la ML y est decompose en deux etapes: une analyse de cas sur des constantes (telle l'instruction «case» de Pascal), et une commutation de l'application avec la construction de filtrage. Cette regle de commutation entre deux constructions de natures differentes induit une geometrie de calcul surprenante, a priori incompatible avec les intuitions habituelles de typage. Cependant il a ete montre que ce calcul est confluent, et verifie la propriete de separation (a la Bohm). Cette these propose un systeme de types du polymorphique pour ce calcul, et decrit ensuite un modele de realisabilite, qui adapte les candidats de reductibilite de Girard au lambda calcul avec constructeurs. La normalisation forte du calcul type et l'absence d'erreur de filtrage lors de l'evaluation en decoulent immediatement. Nous nous interessons ensuite a la semantique du lambda calcul avec constructeurs non type. Une notion generique de modele categorique pour ce calcul est definie, puis un modele particulier (le modele syntaxique dans la categorie des PERs) est construit. Nous en deduisons un resultat de completude. Enfin, nous proposons une traduction CPS du lambda calcul avec constructeurs dans le lambda calcul simplement type avec paires. Le lambda calcul avec constructeurs peut ainsi etre simule dans un calcul bien connu, et cette traduction nous permet aussi de transformer tout modele par continuation en modele du lambda calcul avec constructeurs. Une equation categorique caracteristique de ces modeles apparait alors, qui permet de construire des modeles non syntaxiques (dans les domaines) de Scott du lambda calcul avec constructeurs.