Ces dernières années ont vu une convergence accrue entre langages de programmation fonctionnels typés dont les systèmes de types sont de plus en plus évolués (Haskell, O'Caml, ...) et logiciels de preuve dont l'expressivité calculatoire est de plus en plus calquée sur celle des langages de programmation (Agda, Coq, Twelf, ...), notamment par la présence de constructions sophistiquées de filtrage sur des objets algébriques.
Cette convergence ne va pas sans poser de nombreuses questions théoriques et pratiques. L'une d'elle concerne l'inférence de type que l'on peut voir comme une analyse statique des contraintes qui relient les différentes parties d'un programme entre elles. En présence de types riches, l'établissement de ces contraintes reposent sur des algorithmes d'unification d'ordre supérieur qui, en soit, sont indécidables. L'un des objectifs de la thèse est de concevoir des restrictions réalistes de l'unification d'ordre supérieur qui non seulement sont décidables (notamment en intégrant l'unification « motif » de Miller) mais aussi savent gérer de manière appropriée l'unification en présence de filtrage sur des objets algébriques.
Une autre des questions clés propres aux langages à types riches est la capacité de ces langages à implémenter de manière efficace des effets de bord (affectations, entrées-sorties, partialité, ...) tout en permettant des spécifications riches de ces effets. L'approche standard jusqu'à présent repose sur des interprétations « monadiques » des effets. Or il a été montré (par Filinski) que les monades pouvaient à leur tour être exprimées en « style direct » (donc de manière efficace) via le cadre uniforme des opérateurs dits de « contrôle délimité » (reset/shift), opérateurs dont on vient précisément de prouver qu'ils avaient comme contenu logique le « principe de Markov ». C'est là que se place le second objectif de cette thèse, dans une exploration plus poussée de l'application du principe de Markov et du contrôle délimité à la spécification effective des programmes avec effets de bord et types riches.