I am a researcher at Inria Bretagne within the Ascola Group, 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 am focused on settings more expressive than pure functional programming and intuitionistic logic, often featuring evaluation order.

Subjects I have contributed to, and advocated the unity of, include:

  • Polarisation and focusing, their computational interpretations, and their difference;
  • Operational and equational semantics in the presence of evaluation order, in particular their relationship, and the importance of direct-style and abstract-machine-like calculi;
  • 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 linear logic lens, and the formulae-as-types lens;
  • 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;
  • Computational effects and resources, in particular dependent types in this context;
  • Applications of polarisation to programming language design and implementation;
  • Normalisation-by-Evaluation, completeness proofs, Kripke logical relations.


Young researchers