Après deux ans à l'École normale supérieure de Lyon dans le département d'informatique et un master 2 au MPRI, j'ai été doctorant de l'université Paris Diderot sous la direction de Hugo Herbelin au sein de l'équipe Πr2 à l'origine sur cette thématique.
Ma thèse s'intitule au final De nouveaus outils pour manipuler les inductif en Coq. Les information a propos de sa soutenance sont disponibles sur une page consacrée.
En 2014-2016, Je travaille sur KaSim.
L'avantage du post-doc, c'est de ne pas avoir à enseigner. Pour ne pas (completement) en profiter, je donne des TP de Caml Light en MPSI
What I cannot create, I do not understand.
Richard Feynman (Merci O. Danvy)
En 2010/2011, j'ai réalisé des TP d'initiation à l'informatique en première année de licence de sciences exactes et des TD d'algorithmiques en Master 1 d'informatique.
En 2011/2012 et 2012/2013, mon service a consisté en les Cours/TP d'initiation aux systême d'exploitation en L1 sciences exactes et les TD d'initiation à l'algorithmique pour la licence de BioInfo.
En 2013/2014, J'ai participé aux TP de programmation fonctionnelle et d'analyse lexicale et syntaxique en Licence d'informatique. Je suis aussi en charge des TP de Compilation en master 1.
Durant ma thèse, J'ai passé la majeure partie de mon temps dans le code source de Coq. Les conséquences visibles de cet état de fait sont dans mon manuscrit de thèse. Ils devront être mieux réexpliqué et traduit en anglais très prochainement si je veux conserver un infime espoir d'avoir une carière académique. Par ailleurs, je maintiens la version binaire de CoqIDE pour MacOS. Des nightly builds sont parfois disponibles.
J'ai fait, sous la direction de Romain Demangeon et Sébastien Briais, en juin et juillet 2008, un stage de licence intitulé "Terminaison en PI-Calcul" au sein de l'équipe PLUME du LIP de l'ENS Lyon. Mon rapport est disponible. Peut-être un jour suivront les sources de l'outil de Sebastien Briais que j'ai adapté.
J'ai été de mai à juillet 2009 en stage dans de l'équipe MSP du département Computer and Informations Sciences de l'université de Strathclyde (Glasgow) sous la direction de Conor McBride à propos de décision d'égalité pour le lambda-calcul avec liste dont voici le rapport, les transparents de soutenance et l'état de la preuve Agda (en anglais).
Mon stage de Master 2 qui a précédé ma thèse traitait de filtrage dépendent en Coq. Il a donné lieu à : un rapport et une soutenance comprenant une démo nécéssitant v8.4 pour fonctionner.
Durant mes loisirs, je fais un peu de robotique autour des activités de Planète sciences.
J'ai aussi été le président de l'association des étudiants dont voici le site web.
Par ailleurs, j'ai transmis une partie du virus à ma soeur qui a donc fait le site de sa compagnie de danse.
A titre de délire personnel, ce site respecte les vielles couleurs de la partie enseignement de la charte graphique de l'ENS Lyon.
Ma formation CSS s'est faite là.
La page de Bools est le lien originel qui a conduit à la méthamorphose de ce site en quelque chose de décent, elle se devait donc d'être citée.
Enfin même si son site n'existe pas encore, Maud se devait d'apparaître quelque part.
