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: .


Research activities

I am interested in programming languages, proof theory, category theory, and the connections between them. I see the Curry-Howard correspondence under the lens of paradigms meant to explain similar phenomena occurring in computation and in logic.

My research focuses on settings more expressive than pure functional programming and intuitionistic logic, often featuring evaluation order, at a foundational level. I believe that reconciling type theory with evaluation order will lead to new fundamental insights on logic and computation.

Evaluation order is a phenomenon central to many topics:

  • Polarisation and focusing, their computational interpretations,
  • Operational and equational semantics in the presence of evaluation order, in particular their relationship,
  • Categorical semantics of higher-order computation, in particular call-by-push-value adjunction models of effects, categorical models of linear logic, their relationships and their computational interpretation;
  • Continuation-passing style and first-class contexts, in particular delimited control, type-and-effect systems, and the relationship with abstract machines;
  • The proof theory of classical and intuitionitic logic, in particular through the lens of linear logic, and the lens of formulae-as-types;
  • Classical realizability, ⊤⊤-closed logical relations;
  • Dualities of computation in the above contexts, in particular the (a)symmetry between call-by-value and call-by-name;

Further research interests and subjects of current work include:

  • Denotational semantics and game semantics, in particular event-structure based;
  • Higher-order rewriting and its applications;
  • Computation with effects and resources, in particular dependent types in this context;
  • Applications of polarisation and linear logic to programming language design and implementation;
  • Normalisation-by-Evaluation, completeness proofs, Kripke logical relations.