Doctor in Computer Science
| Nicolas Pouillard Doctor in Computer Science |
By E-mail:
By IM using my E-mail address with Jabber, Google talk (XMPP)
I blog
I also tweet as npouillard
My GPG public key and an older GPG public key
I am particularly interested in the design of programming languages, specifically about functional languages (such as Agda, Haskell and OCaml).
Since September 2008, I am working on safety of languages featuring meta-programming facilities. By meta-programming one means all programs that do manipulate programs. This range from compilers and other code generators (parser generators, boiler plate removers), to theorem provers and proof assistants, but also to static analysis tools and much more.
Technically one tends to focus on a language design, featuring meta-programming as a two levels, heterogeneous language. This means that one can freely declare a new language representation using some kind of advanced data type. One focuses on providing both type safety and binding soundness of the manipulated programs.
On January 13th 2012, I defended my PhD thesis entitled “Namely, Painless: A unifying approach to safe programming with first-order syntax with binders”. All the material: the document, the slides and the development, can be found below. I did my PhD under the direction of François Pottier, at INRIA Paris-Rocquencourt in the Gallium project-team.
[PhD Thesis] Namely, Painless: A unifying approach to safe programming with first-order syntax with binders (PDF)
[Agda Development] Namely, Painless: The NomPa library (Agda Sources) (Agda Sources Archive)
Nameless, Painless (ICFP 2011) (PDF) (Agda Sources) (Agda Sources Archive) (Haskell) (Haskell Document Archive) (LaTeX)
A Fresh Look at Programming With Names and Binders (ICFP 2010)
[PhD defense] Namely, Painless: A unifying approach to safe programming with first-order syntax with binders (Paris 7 University) (PDF) (PDF [fr]) (Haskell)
Namely, Painless (At Marburg University, Programming Languages and Software Technology Group) (PDF) (Haskell)
Nameless, Painless (ICFP 2011 in Tokyo, Japan) (PDF) (Haskell)
A Fresh Look at Programming with Names and Binders (ICFP 2010 in Baltimore, Maryland) (PDF) (Haskell Document Archive)
Meta-programming tutorial at CUFP 2010 (PDF) (Haskell)
A Fresh Look at Programming with Names and Binders (Gallium seminar May 2010) (PDF) (LaTeX) (Haskell Document Archive)
Not So Fresh ML (CANS 2009) (PDF) (LaTeX) (Haskell Document Archive)
Vers des langages plus expressifs et plus sûrs pour la méta-programmation (forum DIGITEO 2011) (PDF) (Haskell)
Experience report: Mirroring reFLect to OCaml (Submitted to ICFP 2009) (PDF)
Agda archive code + agdai files
Abstract
Atoms and de Bruijn indices are two well-known techniques for programming with names and binders. However, using either technique, programming errors are really easy to make. We propose an abstract interface to names and binders that rules out these errors. This interface is implemented as a library in Agda. It allows defining and manipulating term representations in nominal style, in de Bruijn style, in combinations of these styles, and more.
Whereas indexing the types of names and terms with a natural number is a well-known technique to better control de Bruijn indices, we index them with worlds. Worlds are at the same time more precise and more abstract than natural numbers. Via logical relations and parametricity, we are able to demonstrate in what sense our library is safe, and to obtain theorems for free about world-polymorphic functions. For instance, we prove that a world-polymorphic term transformation function must commute with any renaming of the free variables. The proof is entirely carried out in Agda.
This is a long term project. It is not yet ready for public consumption, however contributions and support would be warmly welcomed. The development takes place on github, feel free to fork and send me pull requests. I already used this library for my latest talks (the .hs/.tar.gz files on this page are examples using this library).
I have contributed to these packages as well: data-object, failure, attempt, control-monad-failure, control-monad-attempt.
My favorite contribution to xmonad (the contribution library to be exact) is the TopicSpace extension. It enables to easily have as many workspaces as there are topics you work on; or launching the right applications in the right directory when you go to a topic with currently no windows.
I maintained the Vim keymap included in Yi for a while, along with some syntax highlighters (OCaml, Literate Haskell, Ott).
I have contributed a few patches to the project, for instance I have added the hunk-coloring feature.
Distributed versioning for everyone (PDF trans) (PDF) (LaTeX) (rslide)
In 2009 I assisted François Pottier (giving TDs in french) for his compilation lecture at École Polytechnique (TD material)
I extracted code from the OCaml/Camlp4 lexers to build a lossless, fault-tolerant, keyword independent, correct and complete (as far as testing goes) for the family of Caml dialects. Get more information at the github page for Camllexer.
Overloading, searching for alternatives (PDF) (HTML) (rslide)
Sup is a console-based email client for people with a lot of email.
Ditz work with distributed version control systems.
Rslide is a single file Ruby program, that I used to write reports and presentations. I now use HLaTeX and TDoc instead.
Download rslide
