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.

- .
- Address
- LS2N

UFR Sciences et Techniques

2, rue de la Houssinière, BP 92208

44322 Nantes Cedex 3

France

## News

- March 2018: A proposal to extend the OCaml language with RAII, move semantics and resource polymorphism (PDF).
- Participez aux Journées Nationales Géocal-LAC 2017, les 13 et 14 novembre à Nantes !
- September 2017: I present a talk entitled
*“What term assignments can do for focusing”*at the Fourth Meeting on Structures and Deduction (SD 2017). (Abstract) - June 2017: a note on models of polarised intuitionistic logic arising from ones of linear logic. (HAL).
- May 2017: a note on Curry's style for Linear Call-by-Push-Value (HAL).
- April 2017: I present a talk entitled
*“Duploid situations in concurrent games”*, joint work with Pierre Clairambault, at the GaLoP 2017 workshop. (Abstract) - Feb 2016: I 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 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

- Guillaume Combette
- Xavier Montillet