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.
- June 2017: a note on models of polarised intuitionistic logic arising from ones of linear logic.
- May 2017: a note on Curry's style for Linear Call-by-Push-Value (HAL).
- 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 see the Curry-Howard correspondence under the lens of paradigms meant to explain similar phenomena occurring in computation and in logic.
My research focuses on settings more expressive than pure functional programming and intuitionistic logic, often featuring evaluation order, at a foundational level. I believe that reconciling type theory with evaluation order will lead to new fundamental insights on logic and computation.
Evaluation order is a phenomenon central to many topics:
- Polarisation and focusing, their computational interpretations,
- Operational and equational semantics in the presence of evaluation order, in particular their relationship,
- 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 lens of linear logic, and the lens of formulae-as-types;
- 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;
- Computation with effects and resources, in particular dependent types in this context;
- Applications of polarisation and linear logic to programming language design and implementation;
- Normalisation-by-Evaluation, completeness proofs, Kripke logical relations.
- Guillaume Combette
- Xavier Montillet