Abstract FR:

L'objet de cette these est la formalisation, en vue du typage, d'un langage fonctionnel de programmation et de manipulation d'objets complexes, base sur le syteme fp de backus. Ce langage est donc un langage sans variable, non type et polymorphique. Nous definissons un langage type, le langage fonctionnel sur graphes, dont le langage non type sous-jacent est celui qu'utilise le programmeur. L'idee du langage fonctionnel sur graphes, developpe a l'origine pour la formalisation de la theorie des categories, est qu'une categorie ne doit pas etre consideree comme un ensemble de fleches mais comme un graphe oriente. Le type d'un terme d'un programme type est un graphe de ce langage. Une grammaire permet de verifier si un programme est un terme bien forme du langage type. Nous definissons ensuite le langage utilisateur a partir du langage type en autorisant la suppression des types et l'omission de certaines fleches a caractere naturel dans l'ecriture des termes d'un programme. Enfin, il est propose un algorithme de controle de types qui verifie la correction d'un programme ecrit en langage utilisateur en constituant le programme correspondant en langage type