Abstract FR:

Dans cette thèse, on présente un cadre qui associe la spécification algèbrique de types à l'algèbre de programme. La principale caractéristique de cette approche est fournie par les opérateurs génériques définissables par les utilisateurs qui donnent une grande puissance d'expression aux règles d'équivalence. En particulier, la structure de certains types est contenue implicitement dans des opérateurs génériques comme l'homomorphisme et l'homomorphisme «inverse». Les applications de cette algèbre de programmes typés incluent la preuve de programmes sans induction explicite, et les méthodes de transformation de programmes comme le «folding-unfolding»