Research articles

2024, 2023, 2021, 2020, 2018, 2016, 2014, 2012, 2011, 2010, 2009, 2008, 2007, 2005, 2004, 2003, 2001, 2000, 1990's, 1980's, PhD thesis and other dissertations, dissemination
2024
“An analysis of the constructive content of Henkin's proof of Gödel's completeness theorem” (extended January 2024 version, submitted) (associated OCaml program) (version from 2016) (version from November 2022, with disjunction), in collaboration with Danko Ilik.
2023
“A parametricity-based formalization of semi-simplicial and semi-cubical sets”, in collaboration with Ramkumar Ramachandra, update from December 2023, submitted (Coq formalization).
2021
“On the logical structure of choice and bar induction principles”, in collaboration with Nuria Brede, proceedings of LICS '21 (bibtex) (illustrated summary) (errata, pdf including errata) (Étienne Miquey's formalisation in Coq, up to Theorem 2 and Proposition 8).
2020
“A calculus of expandable stores”, in collaboration with Étienne Miquey, proceedings of LICS '20 © IEEE (bibtex).
2018
“Realizability interpretation and normalization of typed call-by-need lambda-calculus with control”, in collaboration with Étienne Miquey, proceedings of FoSSaCS '18 (bibtex).
2016
“An analysis of the constructive content of Henkin's proof of Gödel's completeness theorem”, in collaboration with Danko Ilik.
2014
“A dependently-typed construction of semi-simplicial types”, Mathematical Structures in Computer Science, 2015 (erratum) (bibtex) (the formalisation in Coq).
2012
“A constructive proof of the axiom of dependent choice, compatible with classical logic”, proceedings of LICS '12 © IEEE (bibtex) (erratum, pdf including erratum) (talk at LICS '12) (the proof in Coq).
Abstract: We show that by restricting Martin-Löf's strong existential elimination (i.e. elimination of dependent sums) to "negative-elimination-free" proofs, one obtains a constructive logic that proves the axiom of dependent choice in a way that remains compatible with classical logic.
“Classical call-by-need sequent calculi: The unity of semantic artifacts”, in collaboration with Zena Ariola, Paul Downen, Keiko Nakata and Alexis Saurin, proceedings of FLOPS '12 © Springer-Verlag (bibtex).
2011
“Pure Type Systems conversion is always typable”, in collaboration with Vincent Siles, appeared in the Journal of Functional Programming, 2011 (bibtex).
“Classical Call-by-Need and Duality”, in collaboration with Zena Ariola and Alexis Saurin, proceedings of TLCA '11 (bibtex).
2010
“An intuitionistic logic that proves Markov's principle”, proceedings of LICS '10 © IEEE (typos) (bibtex entry) (talk at LICS '10).
“Equality is typable in Semi-Full Pure Type Systems”, in collaboration with Vincent Siles, proceedings of LICS '10 © IEEE (bibtex).
“Kripke models for Classical Logic”, in collaboration with Danko Ilik and Gyesik Lee, appeared in the Special Issue on “Classical Logic and Computation”, Annals of Pure and Applied Logic, 2010 (bibtex).
“λ-calculus and Λ-calculus: a Capital Difference”, in collaboration with Alexis Saurin, manuscript, 2010.
2009
“An operational account of call-by-value minimal and classical lambda-calculus in "natural deduction" form”, in collaboration with Stéphane Zimmermann, Proceedings of TLCA '09, LNCS 5608 © Springer-Verlag (errata included) (bibtex).
“Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus”, in collaboration with Gyesik Lee, WOLLIC '09 (bibtex).
2008
“A new elimination rule for the Calculus of Inductive Constructions”, in collaboration with Bruno Barras, Pierre Corbineau, Benjamin Grégoire and Jorge Luis Sacchini, TYPES '08, selected papers, LNCS 5497 (bibtex).
“An approach to call-by-name delimited continuations”, in collaboration with Silvia Ghilezan, Proceedings of POPL '08 (© ACM - posted here by permission of ACM for your personal use - not for redistribution) (errata) (bibtex) (talk at POPL '08).
Abstract: It has been shown by Saurin that de Groote's variant of Parigot's lambda-mu-calculus is strictly more expressive in the untyped case than Parigot's original calculus. We show that this additional expressivity exactly corresponds to adding delimited control so that de Groote's calculus can be seen as the exact call-by-name counterpart of Danvy and Filinski's shift-reset calculus. This "duality" is expressed in the lambda-mu-tp-hat-calculus which is lambda-mu-calculus equipped with a single dynamically-bound continuation variable denoting a resettable toplevel. An equational correspondence having already been proved in A type-theoretic foundation of delimited continuations for call-by-value lambda-mu-tp-hat and Danvy and Filinski's calculus, we simply show here the equivalence between call-by-name lambda-mu-tp-hat and de Groote's calculus. We continue with a comparative study of the operational semantics, continuation-passing-style semantics, and simple typing of both call-by-name and call-by-value versions. Finally, we show the existence of two other canonical calculus of delimited continuations. The first one morally forms an equational correspondance with Sabry's shift/lazy-reset calculus while the second one is a "lazy" version of de Groote's calculus.
“Control Reduction Theories: the Benefit of Structural Substitution”, in collaboration with Zena Ariola, Journal of Functional Programming, 2008 (bibtex).
Abstract: We investigate the differences between Felleisen et al.'s lambda-C-calculus and Parigot's lambda-mu-calculus (presented, for ease of comparison, with a C-like operator, and extended for expressivity, with a toplevel continuation), in their untyped call-by-value variant. Especially, we show that Parigot's structural substitution of evaluation contexts behaves better in many respects than Felleisen et al.'s substitution of reified evaluation contexts. Still, both calculi are operationally equivalent.
2007
“A Type-Theoretic Foundation of Delimited Continuations”, with Zena Ariola et Amr Sabry, Higher-Order and Symbolic Computation, 2007 © Springer-Verlag (bibtex).
This paper is a full and improved version of “A Type-Theoretic Foundation of Continuations and Prompts”.
2005
“On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic”, Proceedings of TLCA '05, LNCS 3461 (erratum) (bibtex) © Springer-Verlag (the typed degeneracy proof in Coq's old syntax).
Abstract: We consider a theory of Sigma-types (i.e. a type theory restricted to strong existential -- sometimes also referred to as strong sum). We show that the quantification domain of the Sigma-types is degenerated (i.e. it is provably reduced to at most one element) in presence of computational classical logic, i.e. in presence of a control operator similar to callcc equipped with standard reduction rules. We how however that the non degeneracy is non derivable if the classical operator is typed and the eta-reduction rule specific to this operator (i.e. "callcck M -> M, for k not occurring in M") is removed.
“Type inference with algebraic universes in the Calculus of Inductive Constructions”, manuscript, 2005.
2004
Abstract: The paper studies call-by-value Parigot's lambda-mu-calculus (where mu is written with a C operator) extended with a dynamically-scoped continuation variable and shows that the resulting calculus is equivalent to Danvy-Filinski shift-reset calculus. The proof is obtained by decomposing Danvy-Filinski double continuation-passing-style interpretation of shift and reset into a state-passing-style transformation followed by a (single) continuation-passing-style transformation. Different type systems are investigated. They are proved to ensure strong normalisation as soon as, either types are decorated with effects, or reset is used on atomic types only. The paper also justifies the subtraction connective as a relevant construction to simulate in a purely functional way the dynamic aspect of a continuation variable such as the one used to interpret reset. Incidentally, a proof of strong normalisation of classical natural deduction extended with the subtraction connective is given. Note that the journal version also repairs the incorrectly stated Proposition 8 from the conference version.
2003
“Minimal classical logic and control operators”, with Zena Ariola, Proceedings of ICALP '03, LNCS 2719 © Springer-Verlag (erratum) (bibtex) (talk in Active dvi format or pdf). A journal version with Amr Sabry entitled "A Proof-Theoretic Foundation of Abortive Continuations" appeared in the Higher-Order and Symbolic Computation journal.
Abstract: Minimal Classical Logic is defined as the restriction of classical logic which enjoys Peirce's Law but not “ex falso quodlibet” (hence not double negation elimination). Typically, Parigot's lambda-mu-calculus is a denotation for the proofs of minimal classical natural deduction. To get full classical logic, we need to extend lambda-mu-calculus with a constant of type absurd. The computational interpretation of this constant is a toplevel continuation. At the end, we give a refinement of Felleisen et al. C operator which allows for a tight correspondence with lambda-mu-calculus.
2001
“Explicit Substitutions and Reducibility”, Journal of Logic and Computation, Vol 11(3), pp 429-449, 2001 © Oxford University Press (the weakening lemma proof in here is wrong... more about it) (bibtex).
Keywords: Lambda-bar-calculus, Explicit Substitutions, Strong Normalisation, Reducibility
Abstract: We define a notion of reducibility based on sequents instead of formulas. We then give a direct proof of strong normalisation for lambda-bar-calculus with explicit substitution.
2000
“The duality of computation”, with Pierre-Louis Curien, Proceedings of ICFP '00 © ACM (get also the errata or ps version that includes the errata, pdf) (bibtex). Later talk to WoLP '04 in advi (install Active dvi) or ps. The notes corresponding to the invited talk at HOR '06 (bibtex).
Keywords: Call-by-Name, Call-by-Value, Sequent Calculus, CPS-Translations Curry-Howard-de Bruijn Proof-as-Program Correspondence, Duality, Lambda-Calculus.
Abstract: We show that the left-right symmetry of Gentzen sequent calculus relates to a duality between terms and contexts and between call-by-name and call-by-value; we design the lambda-bar-calculus, a variant of lambda-calculus which makes these dualities explicit.
1998
“Computing with Abstract Böhm Trees”, with Pierre-Louis Curien, Proceedings of FLOPS'98 (bibtex).
Keywords: Game Models, Abstract Machines, Böhm Trees.
Abstract: We show and compare several variants of abstract machines for weak-head reduction in lambda-calculus, PCF, and, more generally, “abstract Böhm trees”. Some of these machines are expressed in a game setting (e.g. the "geometrical abstract machine" which is new). The other ones are expressed as usual environment machine in KAM-style.
1997
“Games and weak-head reduction for Classical PCF”, Proceedings of TLCA'97 , LNCS 1210 (bibtex).
Keywords: Game Models, Abstract Machines, Classical Logic, Control Operators, Lambda-mu-calculus.
Abstract: We extend Hyland-Ong game model to PCF with catch and throw. It differs from Ong approach in the sense it weakens the rules while Ong adds new moves. We relate also Lorenzen's E-dialogues, Coquand's notion of debate, Krivine Abstract Machine, Parigot's lambda-mu-calculus and game models.
1996
“Game semantics and abstract machines”, with Vincent Danos and Laurent Regnier, Proceedings of LICS'96 (bibtex).
Keywords: Abstract Machines, Game Models for Computation (Hyland-Ong, Abramsky-Jagadeesan-Malacaria), Geometry of interaction.
Abstract: We show that composition in Hyland-Ong model of PCF is linear head reduction in a call-by-name abstract machine. We show that in Abramsky-Jagadeesan-Malacaria model, it is geometry of interaction. The framework of the paper is pure lambda-calculus, not PCF.
“Une caractérisation des stratégies indépendantes de l'histoire à partir des stratégies innocentes”, manuscript, 1996.
Keywords: Game Semantics of Computation (Hyland-Ong, Abramsky-Jagadeesan-Malacaria).
Abstract: We characterise the Abramsky-Jagadeesan-Malacaria "history-free" strategies in terms of Hyland-Ong innocent strategies (in French).
1995
“Notes sur les lambda-sigma-calculs”, manuscript, 1995.
Keywords: Lambda-calculi with Explicit Substitutions, Confluence, non Strong Termination
Abstract: We show that a simple simply-typed lambda-calculus with explicit substitution and composition but no Map rule is enough to get an infinite computation (in French).
1994
“A lambda-calculus structure isomorphic to sequent calculus structure”, Proceedings of CSL'94 (bibtex).
“A lambda-calculus structure isomorphic to sequent calculus structure”, extended version for full classical predicate calculus, draft, 1994 .
Keywords: Sequent Calculus, Proof/program Correspondence (Curry-Howard Correspondence), Lambda-calculi with Explicit Substitution.
Abstract: We extend the proof as program paradigm to Gentzen's sequent calculus. This is done by defining a variant of lambda-calculus with explicit substitution. This new lambda-calculus, the lambda-bar-calculus provides with a term notation for the sequent calculus proofs.
“A-translation and looping combinators in Pure Type Systems”, with Thierry Coquand, Journal of Functional Programming , Volume 4, 1994 (bibtex).
Keywords: Type Systems, Turing's Completeness, Inconsistent Logical Systems.
Abstract: We show that all partial recursive functions are definable in (logical) Pure Type Systems as soon as they are inconsistent (which is the case of Martin-Löf's system Type:Type, Girard's system U, ...) The proof relies on Friedman's A-translation. As a consequence, type-checking is undecidable in Type:Type.
“Some remarks on Novikoff's calculus”, with Thierry Coquand, manuscript, 1994.
Keywords: Classical Logic, Cut-Elimination, Program Extracted from Proofs.
Abstract: We define an interleaving game semantics of products.
1993
“Weak reduction in sequent calculus”, manuscript, 1993, French version integrated in chapter 6 of my PhD thesis.
“Weak cut-elimination and the game-theoretic approach of provability”, manuscript (11 pages), 1993, French version integrated in chapter 6 of my PhD thesis.
1989
“The two-list algorithm for the knapsack problem on a FPS T20”, with Afonso Ferreira and Michel Cosnard, short communication, Parallel Computing , Volume 9, North Holland, 1989 (no electronic version).

PhD thesis and other dissertations

Hab.
“C'est maintenant qu'on calcule: au cœur de la dualité”, habilitation thesis, 2005. Cf specific page.
PhD
“Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes”, PhD thesis, 1995 (errata) (bibtex).
Keywords: Sequent calculus, Cut-Elimination, Lambda-calculi, Game interpretation of provability (Lorenzen's games and Coquand's games), Classical Logic.
Abstract:
We interpret Gentzen's sequent calculus as a lambda-calculus, hence providing a Curry-Howard correspondence for sequent calculus.
We show that Lorenzen's games are just a paraphrase of provability in a particular sequent calculus
We show that cut-elimination in Coquand's game model corresponds to weak-head cut elimination in the modelled sequent calculus.
Mast.
“Formalisation du théorème de Schröder-Bernstein dans le calcul des constructions”, mémoire de DEA, 1988.
Keywords: Formal machine proof, Stratified set theory
Abstract: We formalise Schröder-Bernstein theorem in INRIA's Coq proof assistant (in French).

Dissemination

2017
“Coq, assistant de preuve”, with Sandrine Blazy and Pierre Castéran, Techniques de l'ingénieur, 2017