I am a researcher at Inria Bretagne in the Gallinette team, in Nantes.

I am looking for motivated students and postdocs interested in the topics below. The city and the scientific context are nice.

UFR Sciences et Techniques
2, rue de la Houssinière, BP 92208
44322 Nantes Cedex 3


Research activities

I am interested in proof theory, programming language theory, category theory, and the connections between them. In my view, the Curry-Howard correspondence is an active methodology as much as a foundation. The discovery of similar structures between proofs and programs reveals that there are similar phenomena at work in logic and computation; our work is then to explain these phenomena by developing paradigms, where mathematical abstractions play a crucial role of unification and fertilisation.

In this view, the λ-calculus is a successful and established paradigm of higher-order computation. It takes many forms, such that the paradigm cannot be reduced to a particular formalism. My research focuses on more expressive settings, often featuring “evaluation order”, where the paradigm of the λ-calculus has shown many limitations. In these contexts, one has repeatedly discovered the same structures since the 1960's: so-called “dualities of computation” observed in various topics (operational, categorical and game semantics, the proof theory of classical logic, and proof search). They display a further (“Gentzen-Landin”) correspondence and call for a unifying paradigm of evaluation order, whose current inadequacy is witnessed by idiosyncrasies in our fields. My publications contribute to such a paradigm.

This plays a role in various topics that keep me busy currently:

  • Proof-theoretical coherence,
  • Type theory with evaluation order,
  • Axiomatics of type systems and denotational semantics,
  • Applications of higher-order rewriting,
  • Resource management in programming languages.