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. (Funding available on various theoretical and applied topics related to resource-management in programming languages.) The city and the scientific context are nice.

I am a member of ACM SIGLOG (special interest group in logic and computation). Please promote the ACM Code of Ethics and Professional Conduct.

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



(selected posts)

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 sensitivity to “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 correspondence (of “Gentzen-Landin” if we want) and call for a unifying paradigm of evaluation order, to which my works aim to contribute.

Phenomena, results, and history around it have something to say about 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,
  • Method in programming language research.

These days, I spend time hacking on the OCaml compiler to build the next best systems programming language.

Students (past and present)

  • Adnan Ben Mansour
  • Antoine Defourné
  • Guillaume Combette
  • Xavier Montillet