@PHDTHESIS{moyenthesis,
        CRINNUMBER = {A03-T-513},
        CATEGORY = {9},
        EQUIPE = {CALLIGRAMME},
        AUTHOR  = {Moyen, Jean-Yves},
        TITLE = {Analyse de la complexit{\'e} et transformation de 
programmes},
        SCHOOL = {Nancy 2},
        YEAR ={ 2003},
        TYPE = {Th{\`e}se d'universit{\'e}},
        MONTH ={ Dec},
        KEYWORDS  = {termination, complexity, rewriting, petri nets, 
deforestation},
        ABSTRACT  = {Le th{\`e}me de la th{\`e}se concerne l'analyse 
automatique de la complexit{\'e} des programmes, en particulier en terme 
de complexit{\'e} de la fonction calcul{\'e}e et non de l'algorithme 
impl{\'e}ment{\'e}.  D'une part, la notion d'ordres de terminaison des 
syst{\`e}mes de r{\'e}{\'e}criture est restreinte {\`a} l'aide de 
quasi-interpr{\'e}tations, ce qui permet de donner une borne sur la 
complexit{\'e} de la fonction calcul{\'e}e. Cette borne n'est pas 
n{\'e}cessairement atteinte par le syst{\`e}me {\'e}tudi{\'e} et il peut 
{\^e}tre n{\'e}cessaire de transformer le programme pour l'atteindre. 
Une caract{\'e}risation de PTIME et une de PSPACE sont ainsi obtenues. 
D'autre part, un mini langage d'assemblage est {\'e}tudi{\'e} au moyen 
de r{\'e}seaux de Petri. Il devient ainsi possible de regrouper dans une 
seule analyse une preuve de terminaison proche du ``Size-Change 
Principle'', une preuve de calcul en place (sans allouer de m{\'e}moire 
suppl{\'e}mentaire) et une simplification du programme similaire {\`a} 
la d{\'e}forestation.  De plus, cette technique permet de prouver la 
terminaison d'une tr{\`e}s grande classe de programmes. En particulier, 
la terminaison d'algorithmes comme celui d'Euclide ou comme les 
algorithmes ``Diviser pour r{\'e}gner'' est obtenue de mani{\`e}re 
totalement automatique. },
}