 | Nicolas Pouillard − “Type Theory Hacker” Doctor in Computer Science Current position: free-lance programmer & researcher. Former positions:
|
By E-mail:
I am np on keybase
I also tweet as npouillard (sometimes)
I am npou42 on .
My GPG public key an older GPG public key and an even 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
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.
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.
Dependent Communication in Type Theory (with Daniel Gustafsson and Nicolas Guenot) (PDF)
Dependent protocols for communication (with Daniel Gustafsson) (PDF)
Foldable containers and dependent types (with Daniel Gustafsson) (PDF)
Jesper Borgstrup's Master Thesis: Private, Trustless and Decentralized Message Consensus and Voting Schemes (PDF) (Jesper's page)
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)
Programing with Linear Types, a tutorial (2015, AIM, Göteborg) (HTML) (Markdown)
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)
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.
Vers des langages plus expressifs et plus sûrs pour la méta-programmation (forum DIGITEO 2011) (PDF) (Haskell)
Counting on Type Isomorphisms (with Daniel Gustafsson) [superseded by “Foldable containers and dependent types”] (PDF)
Experience report: Mirroring reFLect to OCaml (with Michel Mauny) (Submitted to ICFP 2009) (PDF)
As part of this project there is two subprojects: explore and agda-nplib
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 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).
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.
I now mainly use Git instead of Darcs.
In 2013 and 2014 I co-lectured the Programming Language Seminar at ITU (IT University of Copenhagen) (links 2014)
In fall 2012, 2013 and 2014 I supervised the “Project Cluster: Programming Workshop” course at ITU (IT University of Copenhagen) (links 2013 2014)
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)
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.
Sup is a console-based email client for people with a lot of email.
I no longer use Sup and switched to notmuch.
Ditz work with distributed version control systems.
I no longer use Ditz.
Rslide is a single file Ruby program, that I used to write reports and presentations. I now use HLaTeX and TDoc instead.
Download rslide
I do not recommend using this tool as there is no longer any development.
I do not recommend using this tool as there is no longer any development.
Solarized color theme by Ethan Schoonover