Pierre Boutillier

English
Moi je

Coordonnées

pierre.boutillier_at_ens-lyon.org

Voici un CV réalisé pour un cours d'anglais.

Études

Après deux ans à l'École normale supérieure de Lyon dans le département d'informatique et un master 2 au MPRI, je suis maintenant 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.

What I cannot create, I do not understand.

Richard Feynman (Merci O. Danvy)

Doctorat

J'enseigne au sein de l'UFR d'informatique de l'université Paris Diderot

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, Je participe au 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.

Coq

Je passe la majeure partie de mon temps dans le code source de Coq. Les conséquences visibles de cet état de fait sont :

Les trois derniers points forment le contenu de 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.

Classical Pure Type Systems

At first my phD was supposed to talk about effect in dependently typed programming languages. Here are some remains:

Following the work of on the one side Barthe, G., Hatcliff, J., Sørensen, M.H.: A notion of classical pure type system. Electr. Notes Theor. Comput. Sci.(1997) 4-59 and on the other side Danvy, O., Filinski, A.: A functional abstraction of typed contexts. Technical Report 89/12, DIKU, University of Copenhagen, Denmark, 1989., we try to define a generic notion of PTS that admit a classical version.

Productions

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.

Autres

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 .

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.

Valid XHTML 1.0 Strict CSS Valide !