Abstract FR:

Cette these aborde certains aspects operationnels fondamentaux des langages fonctionnels et logiques dont le mecanisme d'evaluation est fonde sur la reecriture. Nous etudions deux types de combinaisons de langages de programmation, dont les constituants sont soit des langages de programmation dont le mecanisme d'evaluation est uniquement base sur la simplification, soit des langages de programmation logique et des langages de resolution de contraintes. Le second type est bien connu grace aux travaux de a. Colmerauer, j. Jaffar, et j. -l. Lassez entre autres. Nous en etudions certains aspects originaux, ou le langage de contraintes est purement equationnel et interprete dans un quotient de l'algebre de herbrand. Le premier type est apparu tres recemment, a travers les travaux de v. Brazu-tannen, j. Gallier, f. Barbanera, j. -p. Jouanneaud, et m. Okada. Notre rapport dans ce domaine a consiste pour l'essentiel, d'une part a generaliser aux differents calculs du cube de barendregt des approches au depart restreintes au lambda-calcul type polymorphe, d'autre part a etudier l'impact de l'inference de types sur ce type de combinaison