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

- Décembre 2018: Séminaire au Collège de France,
intitulé
*“Peut-on dupliquer un objet ? Linéarité et contrôle des ressources”*, au sein du cours de Xavier Leroy. Accès libre. - November 2018: I will give an invited talk at
the inaugural
days of the GT Scalp, entitled
*“From systems programming to linear logic, and back”*. (Abstract) - Please send your best science to ICFP 2019!
- June 2018: slides from my talk at the Gallium Seminar entitled
*“A proposal for a resource-management model for OCaml”*. (PDF, June 29th) - May 2018: I will present a talk entitled
*“A resource modality for RAII”*at the workshop on Syntax and Semantics of Low-Level Languages in Oxford, joint work with Guillaume Combette. (Abstract) - 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 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”)
and call for a unifying *paradigm of evaluation order*, to which my
publications
aim to contribute.

Evaluation order 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

- Antoine Defourné
- Guillaume Combette
- Xavier Montillet