Abstract FR:

Recemment, les chercheurs dans le domaine de la theorie de langages de programmation ont remplace la vision usuelle de la substitution par une vision plus fine, en la deplacant du niveau meta (notre langage de discours) vers le langage objet (notre langage d'etude). Cette these s'interesse aux calculs de substitutions au niveau objet, appeles calculs de substitutions explicites (se). Les trois axes d'etude suivants sont developpes : nous considerons d'abord des strategies de reecriture perpetuelles (celles qui preservent la possibilite de derivations infinies) dans le lambda calcul avec se. Nous etudions aussi comment caracteriser inductivement l'ensemble des termes qui terminent et on analyse des proprietes du calcul polymorphe avec se telles que la preservation de types et la terminaison. En second lieu, nous etudions le -calcul d'objets de m. Abadi et l. Cardelli augmente avec des se. Des proprietes telles que la simulation du lambda calcul, la confluence et la preservation de la terminaison sont considerees. Finalement, nous abordons la reduction de la reecriture d'ordre superieur a celle du premier ordre. Nous definissons une variante de la classe des systemes ers de z. Khasidashvili's (appeles ers d b) comme formalisme de depart et nous donnons une procedure de conversion qui permet de coder un ers quelconque dans un systeme du premier ordre dans lequel chaque etape de reecriture se fait modulo une theorie equationelle determinee par le calcul de se. Ce systeme de reecriture est obtenu a l'aide d'une presentation des calculs de se fondee sur des macros. Nous obtenons ainsi une procedure de conversion parametrisee par un calcul de se quelconque qui verifie la presentation mentionnee auparavant. Des proprietes qui mettent en relation la reecriture d'ordre superieur et celle du premier ordre sont etudiees en detail. Nous considerons aussi la possibilite de transferer des resultats du formalisme du premier ordre vers celui d'ordre superieur.