Pierre Boutillier

Francais
My face

Contact

pierre.boutillier_at_ens-lyon.org

I made an old CV during my English lessons

Study

I have been student at the École normale supérieure de Lyon in the Computer Science Department for two years. Then, I studied at the MPRI.

I was PhD student in Université Paris Diderot in PPS lab suppervised by Hugo Herbelin about dependently typed programming inside the Coq proof assistant.

There is a webpage (in French) about my defense.

PostDoc

In 2014-2016, I work on KaSim.

What I cannot create, I do not understand.

Richard Feynman (Merci O. Danvy)

PhD

Teaching in the computer sciences departement of Paris Diderot

I've teached (in french) first year introduction to programming languages and Master 1 algorithmics exercice sessions in 2010/2011.

I've teached (still in french) first year introduction to operating systems and introduction to algorithms for biologic studies in 2011/2012 and 2012/2013.

I teach functionnal programming, parsing and compilation in 2013/2014.

Coq

During my PhD, I spent nearly all my time, hacking coq. The consequences are the contents of my PhD manuscrit (in French). They must be better explained and transalated into articles in a very near future if I want to maintain a slim hope to get one day a position. I also maintain CoqIDE under MacOS. Nightly builds are sometime available.

Production

I made an internship untitled "Terminaison en PI-Calcul" in June and July 2008 in the PLUME team of the LIP at the ENS Lyon under the responsibility of Romain Demangeon and Sebastien Briais. You can download my report (in french) and in a near future the source of Sebastien Briais's software I've adapted.

In 2009, I worked from April to July in the MSP team of the Computer and Informations Sciences departement Strathclyde university (Glasgow) with Conor McBride. I tried to deal with equality over lambda-terms with list primitives. You can find here my report, the slides I used to show my work and the state of the Agda proof.

My master internship that precede my PhD dealed with dependent pattern-matching in Coq. Here is my report, the formal description of the guard condition I proposed and the slides of my defence.

Other

I'm fond of robotics. I randomly do some with Planète sciences.

I have also been the student union's president for a year. Here is our website.

On its bottom, my french page contains privates jokes about what I think an English speaker doesn't care.

Valid XHTML 1.0 Strict CSS Valide !