I am a researcher in computer science at Inria, since January 2015, in the PARTOUT team.
My research topic. I study higher-order computations, the approach to computation where the inputs and the outputs of a program are not simply numbers, strings, or compound data types but also programs themselves. I mainly study the lambda calculus, the mathematical core formalism for higher-order computations, using a combination of tools from logic, graphical syntaxes, rewriting theory, computational complexity, denotational semantics, concurrency, and implementations of programming languages.
The main fields of application are functional programming languages such as OCaml or Haskell, but functional features are nowadays also found in mainstream languages such as Java or Python, and proof assistants such as Coq or Agda. In addition, the lambda-calculus is also of interest for its mathematical connections to proof theory and category theory.
Bird's Eye View. My research work is an attempt to connect different tools and perspectives in the study of the lambda calculus. There are two main recurrent and correlated themes in my work, one of an internal nature and one of an external nature:
Internal: connecting the classical mathematical theory of the lambda calculus with the practice of the implementations of functional languages, by building a mathematical theory of sharing, the crucial ingredient for efficiency;
External: reconciling the schism between the lambda calculus and computational complexity, by studying reasonable cost models for time and space in the lambda calculus.
Both topics have been reshaped by the results that I have obtained in various collaborations. In particular, I was involved in the solution of three long-standing open problems:
Sharing: finding the canonical lambda calculus with first-class sharing. The lambda calculus can be enriched with sharing (or explicit substitutions) in many different ways. Since the 1990s many calculi have been proposed, usually with complex theories and unable to preserve the properties of the lambda calculus. In collaboration with Delia Kesner, I introduced the linear substitution calculus, which is simpler than all previously calculi, preserves the properties of the lambda calculus, and has some properties that the lambda calculus does not (for instance, postponement of garbage collection and confluence in the weak case). See papers [C5,C6,C10,C22] below.
Time: finding the first reasonable time cost model for the lambda calculus. In collaboration with Ugo Dal Lago, I proved that the lambda calculus is a reasonable computational model for time, i.e. that it is polynomially related to Turing machines, see paper [J3] below. Our proof solved a long-standing open problem, and in an unexpected way. The lambda calculus was indeed suspected to be unreasonable because of a negative result due to Asperti and Mairson (in POPL '98). This is my most important contribution, and a major development in the theory of lambda calculus.
Logarithmic space: finding the first reasonable space cost model for the lambda calculus accounting for logarithmic space. Logarithmic space has to be measured via an abstract machine, and it was conjectured that one had to use token-based machines, because environment-based ones could not be space reasonable (that is, equivalent to Turing machines). In collaboration with Ugo Dal Lago and Gabriele Vanoni, we first refuted the conjecture about token-machines in paper [C32] below, and then in [C36] we introduced an environment-based machine that, against expectations, provides the first reasonable cost model for logarithmic space.
My HDR thesis is an overview of 15 years of research (2011-25) that might be a good introduction to my work.
E-mail: "givenname"."familyname" at inria.fr