How to contact me

By E-mail:

By IM using my E-mail address with Jabber, Google talk (XMPP)

In person: my office at ITU is 4C16 (4th floor, corridor C)

I (should) blog

I also tweet as npouillard (sometimes)

I have no account (if you find one under my name that's not mine)

My GPG public key and an older GPG public key

I am npouillard on IRC (freenode, OFTC) and my OTR fingerprint is: F2B8B602 0F30695D 71FE2410 D963C801 D539759D

A signed list of identifiers and fingerprints and the GPG signature

Generally I tend to use logins such as npouillard (reddit, eBay, skype, ycombinator, twitter), np (npmjs, brickset), npou (docker).

Some of my developments can be found on my github page: github.com/np

Research

Research topic: Formal Verification of Cryptographic Schemes

Cryptography and Security have always been my first topic of interest. However functional programming and language design step over and led me to my PhD. I now take the opportunity to get closer to cryptography by applying language design and formal methods to the verification of cryptographic schemes.

With crypto-agda we aim at providing library and language support for developing secure cryptographic code. With crypto-agda, programs are written in a way which enables extraction of circuits, cost analysis, semantic reasoning, and probabilistic reasoning. The extraction to a circuit description enables the programs written with crypto-agda to be run in production. The cost synthesis of the program gives an approximation of running time and memory/size of the circuit. This approximation is made to catch any real exponential behavior of the program, hence capturing the required information about its complexity. Reasoning on programs is enabled by viewing them as Agda functions on which reasoning is already possible. Essentially, the programs considered are only about bit vectors manipulation. Superficially, we provide support for more convenient finite types: products, single bits, vectors... In practice these types provide with a static and versatile system to track vectors sizes. Randomized programs are internally represented as deterministic programs taking the randomness as an extra argument. Externally, the library provides with a set of operations to directly write randomized programs. Probabilistic reasoning about these randomized programs is made easy by this internal representation as well.

Cryptographic primitives and constructions can be described in a functional programming style which is actually pretty close from the descriptions made with diagrams. Security properties are expressed using traditional security games (such as semantic security) involving the so-called “advantage” of a given adversary. These probabilities are computed in a formal and computational way. Our definition for probabilities takes advantage of the pervasive use of finite types for the randomness and puts aside the need for a formalization of real numbers in type theory. Proofs about the security properties are intended to be carried out in three situations. For some basic systems the security actually relies on information theory (such as “one time pad”). For cryptographic primitives which reduce to hard problems. For cryptographic constructions, which combine secure components into a bigger secure component.

The crypto-agda library is still under heavy development. Any comment or question will be welcomed.

Research topic: Language Design, Type Systems and Meta-programming

I am particularly interested in the design of programming languages, specifically about functional languages (such as Agda, Haskell and OCaml).

From September 2008 to January 2012, I was 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.

Drafts

Dependent protocols for communication (with Daniel Gustafsson) (PDF)

Foldable containers and dependent types (with Daniel Gustafsson) (submitted to PPDP2014) (PDF)

Publications

Names For Free — Polymorphic Views of Names and Binders (with Jean-Philippe Bernardy) (Haskell Symposium 2013) (PDF)

A unified treatment of syntax with binders (with François Pottier) (JFP Vol. 22) (PDF) (TeX)

[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 (with François Pottier) (ICFP 2010)

Talks

Breach In Agda (security notions, proofs and attacks using dependently typed functional programming) (2013, 30c3, Hamburg) (HTML) (Markdown)

Names For Free — Polymorphic Views of Names and Binders (Haskell Symposium 2013) (HTML) (Markdown) (CSS) (Build)

fun-universe: Tracking space and time through a restricted universe (AIMXVI) (HTML) (Markdown)

Binder representations in Agda (Invited talk at LFMTP 2012, co-located with ICFP) (HTML) (Agda Archive)

[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)

Distributed versioning & Darcs: Distributed versioning for everyone (PDF trans) (PDF) (LaTeX) (rslide)

OCaml, reFLect and overloading: Overloading, searching for alternatives (PDF) (HTML) (rslide)

Events

AIMXVI: I co-organized the 16th editon of AIM (Agda {Intensive,Implementors} Meeting). If you are interested in type-theory hacking, consider joining the next edition of this meeting.

Posters

Vers des langages plus expressifs et plus sûrs pour la méta-programmation (forum DIGITEO 2011) (PDF) (Haskell)

Unpublished papers

Counting on Type Isomorphisms (with Daniel Gustafsson) [superseeded by “Foldable containers and dependent types”] (PDF)

Experience report: Mirroring reFLect to OCaml (with Michel Mauny) (Submitted to ICFP 2009) (PDF)

Personal interests (non-exhaustive)

Technical

Social

Agda Hacking

crypto-agda: A library for defining cryptographic schemes and proving security properties.

crypto-agda on GitHub

As part of this project there is two subprojects: explore and agda-nplib

NomPa: A library for safe and expressive programming with names and binders.

Agda archive code

Agda archive code + agdai files

Agda HTML code

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.

Haskell Hacking

HLaTeX: A LaTeX document builder for Haskell

This is a long term project. It is not really as I would like it to be 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 PhD, two articles and all my recent talks (the .hs/.tar.gz files on this page are examples using this library).

Hackage contributions

I have contributed to these packages as well: data-object, failure, attempt, control-monad-failure, control-monad-attempt.

xmonad is a dynamically tiling X11 window manager that is written and configured in Haskell

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.

Contributions to Yi: a text editor written and extensible in Haskell

I maintained the Vim keymap included in Yi for a while, along with some syntax highlighters (OCaml, Literate Haskell, Ott).

Contributions to Darcs: an advanced distributed revision control system

I have contributed a few patches to the project, for instance I have added the hunk-coloring feature.

I now mainly use Git instead of Darcs.

Teaching

In fall 2012 and 2013 I supervised the “Project Cluster: Programming Workshop” course at ITU (IT University of Copenhagen).

In 2012 and 2013 I co-lectured the AMP (Advanced Models and Programs) course at ITU (IT University of Copenhagen)

In 2009 I assisted François Pottier (giving TDs in french) for his compilation lecture at École Polytechnique (TD material)

OCaml Hacking

Camllexer: A standalone lossless lexer for OCaml like languages

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.

ocamlbuild

Camlp4 bazaar

Ruby Hacking

Contributions to Sup

Sup is a console-based email client for people with a lot of email.

I no longer use Sup and switched to notmuch.

Contributions to Ditz

Ditz work with distributed version control systems.

I no longer use Ditz.

Rslide: A lightweight LaTeX/HTML generator

Rslide is a single file Ruby program, that I used to write reports and presentations. I now use HLaTeX and TDoc instead.
Download rslide

Uttk: Unified Test Tool Kit

I do not recommend using this tool as there is no longer any development.

Vcs: A wrapper over Version Control Systems

I do not recommend using this tool as there is no longer any development.


I'm a Haskeller

View Nicolas Pouillard's profile on LinkedIn

Valid HTML 5.0!Valid XHTML 1.1!Valid CSS!

Solarized color theme by Ethan Schoonover

Powered by Haskell (TDoc)