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. (Funding available on various theoretical and applied topics related to resource-management in programming languages.) The city and the scientific context are nice.
I am a member of ACM SIGLOG (special interest group in logic and computation)... 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
News
- May 2020: Towards better systems programming in OCaml with out-of-heap allocation (draft).
- 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)
- 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.
Blog
(selected posts)- 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.
- De-allocation is a side-effect, January 3rd 2020.
- Abstraction vs. efficiency of continuation-passing style, October 18th 2019.
- An original use of GC alarms in OCaml, September 25th 2019.
- 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.
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” if we want) and call for a unifying paradigm of evaluation order, to which my works aim to contribute.
Phenomena, results, and history around it have something to say about 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,
- Method in programming language research.
These days, I spend time hacking on the OCaml compiler to build the next best systems programming language.
Students (past and present)
- Adnan Ben Mansour
- Antoine Defourné
- Guillaume Combette
- Xavier Montillet
Co-authors
- Pierre-Louis Curien
- Rémi Douence
- Marcelo Fiore
- Gabriel Scherer
- Étienne Miquey
- Xavier Montillet