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

## News

- Apr 2016: a draft for a long version of the POPL 2016 paper.
- Feb 2016: Slides for my talk at POPL are available.
- October 2015: I will present the
paper
*A Theory of Effects and Resources: Adjunction Models and Polarised Calculi*, joint work with Marcelo Fiore and Pierre-Louis Curien, at the*43rd annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*(POPL 2016). - June 2015: The
paper,
*Polarised Intermediate Representation of Lambda Calculus with Sums*, joint work with Gabriel Scherer, to be presented at the*Thirtieth Annual ACM/IEEE Symposium on Logic In Computer Science*(LICS 2015), is available on HAL. - July 2014: I have appended the proofs from my PhD thesis
referred to in my
paper
*Formulae-as-Types for an Involutive Negation*, accepted for the*Joint meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science*(CSL-LICS). - June 2014: The slides for the
first part of my talk entitled
*Polarities and classical constructiveness*, at the Institut Henri Poincaré thematic trimester on Semantics of proofs and certified mathematics, are available. For the second part, see my talk at FOSSACS. - February 2014: The LaTeX package perfectcut.sty is now hosted on CTAN and is available via TeXLive and MiKTeX.
- July 9th 2012: added to the note Λ-calcul, machines et orthogonalité a comparison of Krivine's “adapted pairs” technique to the orthogonality technique.

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