gallais

Présentation

Je prépare en ce moment une thèse sur la programmation avec types dépendents sous la direction de Conor McBride au sein du groupe MSP de l'Université de Strathclyde (Glasgow - Écosse).

Sujets de prédilection

Je m'intéresse tout particulièrement à la théorie des types. La majeure partie de mon activité de recherche est centrée à l'heure actuelle autour de l'utilisation de systèmes de types pour maintenir des invariants, aider le programmeur à produire du code correct par construction ou faire en sorte que l'utilisateur d'une bibliothèque ne puisse pas invalider par inadvertance des préconditions vitales. Je suis passionné par la construction de procédures de normalization basées sur différentes techniques de construction de modèles, le développement d'algorithme certifiés de recherche de preuve ou la construction d'univers internalisant certaines propriétés souhaitables. Mes langages de programmation préférés sont Agda, Haskell et OCaml.

Par le passé, j'ai beaucoup travaillé en Coq (formalisation d'une bonne tranche d'analyse réelle en rapport avec les séries entières) et Isabelle (certification de preuves de terminaison produites par des outils automatiques).

Dépots


Dernière màj : 2014 07 28
fun