I am an assistant professor at LIX and a member of the PARTOUT team within the Proofs and Algorithms pole. Previously, I was a Birmingham Fellow at the University of Birmingham for three years, and a member of the vibrant Theory Group in the School of Computer Science. I moved back to France in 2020 to rejoin my wife, after a few years of tricky navigation between Birmingham and Paris.

Before that, I was an itinerant postdoc for around seven years, first in Paris at Laboratoire PPS (now IRIF ) with a fellowship of the Fondation Sciences Mathématiques de Paris, then at IMDEA Software in Madrid, then at the Institute for Advanced Study in Princeton during the special year on Univalent Foundations, and then back to Paris at the MSR-Inria Joint Centre and as a member of Team Parsifal.

And before all that I was a PhD student at CMU SCS, spending six great years in Pittsburgh, Pennsylvania.

Research Interests

I am interested broadly in connections between logic, language, and computation. More specifically, in my research I strive to identify and understand the basic mathematical structures underlying the design, implementation, and analysis of programming languages, using tools such as category theory and proof theory. More generally, I am interested in how all this fits within the broader world of mathematics and computer science.

A long-running project which I’ve been collaborating on seeks to develop a common mathematical language that unifies the disparate traditions of Hoare Logic, dependent type theory, and linear logic. One conclusion reached from this project is that the established wisdom about the /relationship/ between type theory and category theory needs to be revised, and that this has important implications for the way we look at type systems and other deductive formalisms. You can find out more about this view in my paper with Paul-André Melliès, “Functors are Type Refinement Systems” (POPL 2015). Turning this vision into a practical reality will require a lot of work, but I’m convinced that the path ahead will be exciting!

Since more recently (and as an unexpected side effect of the above project) I have also been very interested in understanding some striking connections between lambda calculus and combinatorics, particularly the combinatorics of /maps/ first worked out by Bill Tutte. (The term “map” has different senses in mathematics, but here it is meant in the cartographic sense of a /subdivision of a surface into regions/.) You can have a look at my talk on Lambda Calculus and the 4CT (or watch this video ) for a quick introduction to this fascinating world.

An older interest I have is in the notion of zero-knowledge proof from cryptography/complexity theory, in particular how it can be reconciled with notions of knowledge from constructive logic. I gave a talk about these connections at HOPE 2012, which you can find in “Recent talks”.

If you are potentially interested in PhD research on any of these or related topics you can contact me explaining your interest, although you should be aware that finding funding to sponsor a PhD in France can be tricky and requires a good sense of timing.