Abstract FR:

Cette these traite du suivi de sujet dans des systemes formels decrits par des systemes de semantique naturelle. Le chapitre un introduction, presente le probleme de suivi de sujet c'est-a-dire la recherche des expressions manipulees dans le programme execute. Le chapitre deux decrit le formalisme utilise pour representer les occurrences dans les arbres, les termes d'un systeme de reecriture et les arbres de preuve. Le chapitre trois etudie les systemes de reecriture lineaires gauches et principalement leur representation par des regles d'inferences. La notion de residu d'occurrences y est rappelee. Le chapitre quatre introduit la notion de marquage, qui permet d'etablir une fonction reliant les occurrences du terme final d'une derivation aux occurrences du terme initial. Un tel marquage permet de garder l'origine de toutes les expressions. Un langage de fonction de marquage est defini et les proprietes algebriques de ce langage sont etudiees. Le chapitre cinq decrit le calcul des fonctions de marquage simultanement au developpement des reductions d'un terme par un systeme d'inference. La methode utilisee consiste a enrichir les regles du systemes d'inference en associant aux reecritures les fonctions de marquage correspondantes. Plusieurs methodes sont presentees, dont la plus generale utilise des informations de flux de donnees pour calculer la provenance des expressions. La correction de ces methodes d'enrichissement est formellement etablie dans ce chapitre. Le chapitre six montre comment ces calculs sont effectivement mis en uvre dans le systeme centaur et dans le langage typol. Le chapitre sept decrit une extension non triviale du calcul des fonctions de marquage au lambda-calcul. Des applications aux langages de programmation sont ensuite decrites