I am a researcher at INRIA in the Gallinette team in Nantes.

I am looking for motivated students interested in the topics below. The city and the scientific context are nice.

I am a member of ACM's Special Interest Group on Logic and Computation (SIGLOG). Please promote the ACM Code of Ethics and Professional Conduct.

E-mail

I cannot guarantee to reply in a timely manner, but feel free to retry after some time. However, I make sure to reply to letters sent to the physical address below.

• LLM policy: I do not reply to messages that seem partially or totally generated by an LLM.
• Review policy: as a signatory of No free view? No review!, I volunteer my time in priority in favour of diamond open access venues (e.g. Episciences), gold open access venues with reasonable fees (e.g. LIPIcs), and nice workshops without proceedings. I also ask that there is an opposable LLM policy for authors and reviewers.
• Antispam: the antispam at INRIA is rather aggressive, as it is in many places nowadays. One should not assume that e-mails always reach their recipients, nor that the sender is notified when an e-mail is not delivered. This is an ongoing issue that has been reported to INRIA's IT services.

Address

LS2N — UFR Sciences et Techniques
2, rue de la Houssinière, BP 92208
44322 Nantes Cedex 3, France

In this page

1. Some news (chronological)
2. Blog (selected posts)
3. Research topics
4. Colleagues

Research topics

I am interested in scientific aspects of computing and reasoning, in particular proof theory, programming, and the connections between them. (If this does not ring any bell, skip the rest and enjoy this nice video by Veritasium: Math's Fundamental Flaw.)

In particular the Curry-Howard correspondence, the connection between some aspects of programming languages and some aspects of mathematical proof systems, is in my view 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, for which much remains to be explained and explored, providing opportunities for fertilisation and unification.

A paradigm of evaluation order

In this view, the λ-calculus, a formal system for representing computation based on the notions of λ-abstractions (functions) and application, is a successful and established paradigm of higher-order computation. It takes many different forms in various areas of research, such that it cannot be reduced to a particular formalism. My research focuses on more expressive settings, often featuring sensitivity to evaluation order, where the λ-calculus has shown many limitations.

In this context, one has repeatedly discovered similar phenomena since the 1960's, so-called “dualities of computation”, arising from the symmetry and the opposition between the player and an opponent in a game or in an argument (observed within various approaches: operational, categorical and game semantics, continuations, proof theory of classical logic, and proof search). It shed light on further connections, for instance between sequent calculus and abstract machines (a “Gentzen-Landin” correspondence, if we want).

Thanks to the efforts of many researchers, we have seen appearing a unifying paradigm of evaluation-order-sensitive computation (see for instance some of the early works by Melliès on tensor logic). My PhD thesis* is written from this viewpoint; its main result characterises sensitivity to evaluation order in many models as a (meaningful) lack of the associativity of composition*.

Two prototypical examples of this understanding of order-related phenomena are, in proof theory, Girard's constructive classical logic, which gives a meaning to reasoning by contrapositive by means of an interpretation into linear logic, and in programming, the fruitful decomposition of various semantics for side-effects into so-called call-by-push-value models.

Linear call-by-push-value is a common decomposition of both, that aims to describe the interaction between linearity—the control over the erasure and duplication of data and computation—and side-effects*. It consists in adding a notion of resource modalities to call-by-push-value for controlling the copying and discarding of values; equivalently it refines intuitionistic linear logic with a sensitivity to evaluation order.

Between functional and systems programming

An important case study of what precedes are types with an ownership constraint, and the representation of resources as values, as popularized by modern systems programming languages (C++11 and Rust). The notion of type with an associated destructor that these languages feature (a function that describes how to perform clean-up upon exiting a scope) can be analysed under the lens of an algebraic construction giving rise to a particular resource modality*. It solves a long-standing question of dealing with the interaction between linearity and control effects in programming language semantics.

This modelling accounts for many interesting observations about resources in C++11 and Rust, most prominently for an interpretation as non-commutative algebraic datatypes (e.g. if the order of destruction at types A and B matters, the tensor product A⊗B is not isomorphic to B⊗A)*. The model lets us distinguish essential from accidental aspects of resource-management in C++11 and Rust, and distill this notion into a proposal to extend ML with resources as first-class values and ownership types*.

Given the importance of this case study, I am now investigating the mixing of systems programming and functional programming (with an evidence-based mindset, by looking at real programs), and I also devote some of my time contributing to the OCaml language.

Other topics

I am more broadly interested in all scientific aspects of computing and reasoning, but more realistically by topics touched upon by the Curry-Howard correspondence, including (but not limited to):

• Type theory, proof theory, and their interactions (e.g. impredicativity, classical reasoning, effects in type theory)
• Linearity in logic, especially modern approaches (probabilistic, differential and tensor logic), and applications to more traditional topics (e.g. proof search)
• Linearity-related approaches in programming languages (ownership types, control of aliasing)
• Some approaches to game semantics
• Applictions of proof theory to category theory (e.g. proof-theoretical coherence)
• Applications of higher-order rewriting
• Systems programming, functional programming, and their interactions
• Method in programming language research

My research sometimes involves artifacts, which are never topics per se, including but not limited to: focused proof systems, polarised logics, term assignments for sequent calculus, call-by-push-value, continuation-passing style transformations, control operators (delimited or not), orthogonality-based logical relations.

Colleagues

Students (current or former, internships or PhD)

• Jean Caspar
• Éléonore Mangel
• Sidney Congard
• Adnan Ben Mansour
• Rosalie Defourné
• Guillaume Combette
• Xavier Montillet

Co-authors

• Jean Caspar
• Sidney Congard
• Pierre-Louis Curien
• Rémi Douence
• Marcelo Fiore
• Éléonore Mangel
• Paul-André Melliès
• Étienne Miquey
• Xavier Montillet
• Gabriel Scherer