I am looking for motivated students and postdocs interested in the topics below. The city and the scientific context are nice.
- Apr 2016: a draft for a long version of the POPL 2016 paper.
- Feb 2016: Slides for my talk at POPL are available.
- October 2015: I will 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.
I am interested in programming languages, proof theory, category theory, and the connections between them. I am focused on settings more expressive than pure functional programming and intuitionistic logic, often featuring evaluation order.
Subjects I have contributed to, and advocated the unity of, include:
- Polarisation and focusing, their computational interpretations, and their difference;
- Operational and equational semantics in the presence of evaluation order, in particular their relationship, and the importance of direct-style and abstract-machine-like calculi;
- Categorical semantics of higher-order computation, in particular call-by-push-value adjunction models of effects, categorical models of linear logic, their relationships and their computational interpretation;
- Continuation-passing style and first-class contexts, in particular delimited control, type-and-effect systems, and the relationship with abstract machines;
- The proof theory of classical and intuitionitic logic, in particular through the linear logic lens, and the formulae-as-types lens;
- Classical realizability, ⊤⊤-closed logical relations;
- Dualities of computation in the above contexts, in particular the (a)symmetry between call-by-value and call-by-name;
Further research interests and subjects of current work include:
- Denotational semantics and game semantics, in particular event-structure based;
- Higher-order rewriting and its applications;
- Computational effects and resources, in particular dependent types in this context;
- Applications of polarisation to programming language design and implementation;
- Normalisation-by-Evaluation, completeness proofs, Kripke logical relations.