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.

E-mail
.
Address
LS2N
UFR Sciences et Techniques
2, rue de la Houssinière, BP 92208
44322 Nantes Cedex 3
France

News

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.

Students

Co-authors