I am a researcher at INRIA 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.
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.
- Address
- LS2N
UFR Sciences et Techniques
2, rue de la Houssinière, BP 92208
44322 Nantes Cedex 3
France
In this page
News
- I am pleased to present two talks at ML 2024 on September 6th:
- “Designing interrupts for ML and OCaml” (joint work with Leo White and Stephen Dolan),
- “Is there a use for linear types?”
- The Onward! conference is held in Pasadena in October 2024. Please submit a paper! (Deadline: April 25th.)
- ML 2024: The ACM SIGPLAN workshop Higher-order, Typed, Inferred, Strict: ML Family Workshop 2024 (or simply ML workshop) is held in Milan on September 6th 2024. Please submit a talk proposal! The deadline is June 6th.
- Our paper entitled “Modular efficient deconstruction with typed pointer reversal” (PDF, HAL), joint work with Jean Caspar (and based on his L3 internship work), has been accepted at JFLA 2024. My student Sidney Congard also presents a paper entitled “Towards a linear functional translation for borrowing” (HAL).
- I co-organize the Undone Computer Science conference, to be held in Nantes on Feb. 5-6 2024.
- I am pleased to present my Resource Polymorphism proposal to extend ML with first-class resources at the ML Workshop on September 8th. (Slides, long version)
- ML'23: The ACM SIGPLAN ML Family Workshop is held in Seattle on September 8th 2023. Please submit a talk proposal!
- Slides for my talk entitled “Programme for a rational reconstruction of ownership in PLs”: 8th February 2023 at ProgLang@Inria, 15th February 2023 at the Scalp Working Group Days.
- September 2022: this paper (PDF) on the OCaml-Rust interface presented at the ML workshop in Ljubljana (HAL). Another presentation at the OCaml workshop on the large pages experiment mentioned below (draft paper (PDF), HAL).
- June 2022: slides of a talk at Inria Paris on the OCaml-Rust interface.
- August 2021: I presented my work entitled Probabilistic
resource limits, or: Programming with interrupts in OCaml,
at
the OCaml
2021 workshop, showing how to correctly program with
asynchronous exceptions with resource-management features in ML,
using my OCaml
package
memprof-limits
. - March 2021: OCaml RFC “Movable roots for a more efficient and more flexible FFI”, joint work with the ocaml-rust team. See also the investigation on callee-roots vs caller-roots in the OCaml-Rust interface.
- May 2020: Towards better systems programming in OCaml with out-of-heap allocation, presented at the ML 2020 Workshop.
- Our TYPES 2020 submission, entitled “Dependent Type Theory in Polarised Sequent Calculus” (PDF/HAL, joint work with Étienne Miquey and Xavier Montillet) was due to be presented in Turin. (Event unfortunately cancelled.)
- The 9th International Workshop on Aliasing, Capabilities and Ownership (IWACO'20) is held in Berlin in July 2020. Please submit a talk proposal!
- January 2020: I presented a course entitled “An opiniated introduction to Call-by-Push-Value” at the Coq Andes Summer School 2020. Here are the slides (PDF).
- July 2019: I will present a work entitled “Efficient Deconstruction with Typed Pointer Reversal” at the ML 2019 workshop, joint work with Rémi Douence. (HAL)
- 13 juin 2019, exposé au séminaire Codes Sources, LIP6: « Curry-Howard et méthode en recherche en langages de programmation : l’exemple de l’objet comme valeur linéaire ».
- The fifth International Workshop on Structures and Deduction is held in Dortmund on 29-30th June 2019. Please submit a talk proposal!
- The tenth workshop on Syntax and Semantics of Low-Level Languages (LOLA 2019) is held in Vancouver on June 23rd 2019. Please submit a talk proposal!
- 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 work entitled “A resource modality for RAII” at the workshop on Syntax and Semantics of Low-Level Languages in Oxford, joint work with Guillaume Combette. (HAL),
- March 2018: A proposal to extend the OCaml language with RAII, move semantics and resource polymorphism (PDF, ArXiv).
- 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, Slides)
- Feb 2016: Slides for my talk at POPL are available.
- 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.
- April 2014: The slides of my talk at FOSSACS entitled Models of a Non-Associative Composition are now available.
- February 2014: The LaTeX package perfectcut.sty is now hosted on CTAN and is available via TeXLive and MiKTeX.
- December 2013: My paper entitled Models of a Non-Associative Composition was accepted for the 17th International Conference on Foundations of Software Science and Computation Structures (FOSSACS).
- December 10th 2013: I defended my PhD thesis entitled Syntax and Models of a non-Associative Composition of Programs and Proofs.
- 11 octobre 2013: la note du GdT Logique de mars 2012 (enfin!).
- July 18th 2013: I wrote the LaTeX package perfectcut.sty to make cuts of system L more readable when nested.
- July 9th 2012: added to the note Λ-calcul, machines et orthogonalité a comparison of Krivine's “adapted pairs” technique to the orthogonality technique.
- 2006: Informatique ENS 2003 — Corrigé partiel de l'épreuve d'informatique du concours d'entrée aux ENS, année 2003.
Blog
(selected posts)- OCaml, large pages, and the cost of a page table, May 2nd 2021 (subsumed by my OCaml workshop 2022 submission).
- A Rust-inspired idea for making the concurrent multicore OCaml GC API-compatible, June 6th 2020.
- Announcing memprof-limits (and a guide to handle asynchronous exceptions), May 14th 2020 (subsumed by my ML workshop 2021 submission).
- De-allocation is a side-effect, January 3rd 2020.
- An audit of asynchronous exceptions in OPAM packages, August 15th 2019.
- Interfacing OCaml with smart pointers, April 19th 2019.
- A proposal for an exception-safety model in multicore OCaml inspired by Rust, November 4th 2018 (subsumed by my ML workshop 2021 submission).
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 (past and present)
- Jean Caspar
- Éléonore Mangel
- Sidney Congard
- Adnan Ben Mansour
- Rosalie Defourné
- Guillaume Combette
- Xavier Montillet
Co-authors
- Pierre-Louis Curien
- Rémi Douence
- Marcelo Fiore
- Gabriel Scherer
- Étienne Miquey
- Xavier Montillet
- Jean Caspar