Abstract FR:

Les calculs de substitutions explicites, offrent un intermediaire entre le lambda-calcul et son implantation. Ils ont ete utilises avec succes pour la conception et la preuve de correction de machines abstraites, l'unification d'ordre superieur ou encore pour la construction incrementale de preuves. Cette these est fondee sur le calcul de substitution explicite de hardin et levy, qui est le seul calcul a ce jour qui soit confluent sur les termes ouverts (ou meta-termes). Elle explore ce formalisme suivant trois axes : 1. La reecriture d'ordre superieur. Dans un premier temps nous montrons que l'adjonction de symboles et de regles confluentes du premier ordre conserve la confluence du calcul de hardin-levy. Nous developpons ensuite un formalisme de reecriture d'ordre superieur, baptise explicit reduction system, dont les mecanismes de substitution sont ceux du calcul avec substitution explicite etendus a des lieurs quelconques. Nous definissons une notion d'arite de liaison basee sur le comportement du passage de la substitution a travers les lieurs. Des conditions suffisantes sont donnees pour la confluence. 2. La theorie de la demonstration. Dans cette partie, nous nous sommes attaches a decrire le systeme de deduction associe par isomorphisme (a la curry-howard) au calcul de hardin-levy. Nous obtenons un calcul equivalent a la deduction naturelle et le nommons calcul de multi-sequents avec variables de jugement. Il permet de manipuler conclusions ou hypotheses ainsi que des variables de preuve. 3. La compilation. Nous montrons comment les calculs de substitutions explicites permettent de representer des machines abstraites, leur correction et la strategie qu'elles suivent. Nous decrivons en detail quatre machines abstraites : la kam, la secd, la cam et la fam. Pour cette derniere, nous montrons comment les substitutions explicites sont utiles pour exprimer la compilation de programmes fonctionnels.