A short presentation of the various young people that regularly gather (or used to gather) at the conversation-rich and often surprising coffee breaks we have at Gallium: les dix gagas.

Onsite Gallium PhD students

In decreasing order of elderness:

  • Jonathan Protzenko had the idea of this blog. He is working with François Pottier on programming language approaches to have finer control of mutability and aliasing. He also hacks for Mozilla on his spare time (eg. he’s the author of the world-famous Conversations extension for Thunderbird) and even wrote a full book about XUL in his young age, before seeing the truth of functional programming. From these fond experiences he’s formed a strong sense of contribution to the community, which makes him an asset of the OCaml bug triaging volunteer squad. Let’s just add that he took responsability for the Windows installer, to give you an idea of his sense of self-sacrifice. His is also in charge of the “junior seminar” here at INRIA Rocquencourt, a great opportunity for students to practice their communication skills, that I hope this blog will complement.

  • Fixing Windows bugs is rarely a charming activity, and Jonathan’s mood sometime pays for it. Julien Cretin is the ever-smiling one. He works on coercions (that is, in his mind, mostly anything typing-related) with Didier Rémy but is in fact busy preparing the revolution: anytime soon programmers will stop using term syntax and variables, and instead draw graphs. He’s also an asset for our cultural diversity, as his main working language is Haskell; he had the luck to do an internship in MSR Cambridge last year, where he helped a dream team to promote Haskell (PDF) through kind-level programming.

  • I’m Gabriel Scherer and I should be working on module systems, also with Didier Rémy. In fact, I’m trying to recover from a serious illness: the inability not to answer a question on the Internet – or comment on a good post. Please also don’t approach me with interesting research topics (anything programming language related), I’m much too likely to get distracted.

  • Jacques-Henri Jourdan started as a PhD student just a few weeks ago. He has already worked in Gallium as an intern, on a formal correctness proof from a grammar description (in Coq, automatically translated from a Menhir grammar) to a LR automaton. He will now work on mechanized formalizations of abstract interpretation techniques.

Stranger beings

  • Alexandre Pilkiewicz found that writing a PhD thesis was too easy, and decided to simultaneously start a job at Google. Here, he was working on formalizing compiler optimizations based on polyhedral loop analyses. He is very comfortable with Coq, to the point that he once did a formal proof of correctness for a small patch I proposed for the standard Map data structure, just for fun.

  • Valentin Robert worked as an intern with Xavier Leroy on Compcert, first on a certified pointer analysis pass, and then on test programs to verify the work of the external non-verified toolchains that take Compcert proved-correct assembly output and generate a real executable. He is our meme expert, and notoriously indecisive. After much hesitation, he will be leaving us in a few months to do a PhD in San Diego.

  • Raphael Proust is the most recent intern in the team; he will be working with Xavier Leroy on the intermediate representations (in a compiler) of functional languages : CPS, SSA, ANF etc. He previously worked with the Mirage team in Cambridge, doing OS-level development in OCaml, and will probably go back there to start a PhD in a few months. That’s a very interesting project with not-so-surprising ties to programming language research; for example he worked on the use of Limel (PDF), a programming language with linear type, to faithfully encode the constraints on low-level dataflow tasks in a networked system.

Recent former students

I won’t list all the former students of Gallium, but here are those I had the pleasure to meet while they were still on duty.

  • Nicolas Pouillard is our former “cultural diversity” leader, using Agda as his proving tool of choice. Coq and OCaml are more in the culture of the place, but anyone is free to choose – and XMonad is certainly king among the window managers used. Nicolas worked on the hairy subject of representing and formally reasoning on syntactic terms with binders. He was also our local expert on practical uses of secure design or cryptography, such as security by capabilities (a hobby I share), web privacy, BitCoin, Tahoe-LAFS… He is now a post-doc at ITU Copenhaguen as part of the demtech project on “trustworthy democratic technology”.

  • Tahina Ramananandro worked on the craziest topic one could find. What is the hardest way to describe a programming language? I would say it is writing mechanized formal semantics for it. What is the most insanely complex language a twisted mind could want to describe? C++. At the end of a truly heroic effort, Tahina had a formalized semantics of memory layout of structs/classes and construction/destruction of objects. He’s now doing a post-doc in the FLINT group at Yale.

  • Benoît Montagu worked on module systems with Didier Rémy. He studied several ways to enhance Fω with some orthogonal features each adding some aspect of the ML module system. He’s now a post-doc in Philadelphia, as part of the quite exciting CRASH/SAFE project. Take a bunch of type system and formal proof experts, and ask them to design an end-to-end (hardware and software) system aimed for security, safety and reliability; they produce a dynamic language.