Recherche

Research

My main research field is theoretical computer science: mathematical logics, theory of programming and computation, and their intertwining along the lines of the Curry-Howard correspondence. You'll find below a list of my papers and my talks on these topics. Besides, I have some (modest) background and (under-exploited) interests in the fields of sociology and law, see the corresponding section for some details.

My original background is proof theory (mostly substructural logics, like linear logic) as well as operational and denotational semantics of the λ-calculus (or variants of it).

• During my PhD with Lionel Vaux Auclair, I have been reformulating the linear approximation of functional programs (aka Taylor expansion for the λ-calculus) using infinitary rewriting T1, J1, J2.
• I am currently working with Giulio Manzonetto and Alexis Saurin on refinements of this program approximation and the associated quantitative semantics, to capture (non-)erasure of data along infinite computations J3.

More generally, I have a strong interest in studying infinite objects and processes that appear in computer science, e.g. using infinitary terms and rewriting, coinduction, fixed points.

• The first part of my postdoc with Ugo Dal Lago is concerned with logical characterisations of productivity for stream programming.
• During my PhD, I worked on a nominal syntax for mixed inductive-coinductive data types with variable binding P3. I've also been investigating coinductive infinitary rewriting of non-wellfounded derivations with Alexis Saurin P4.
• I work on other projects with Pierre Guillon and Lionel Vaux Auclair (on dynamical and computability properties of infinitary rewriting systems), and with Paul-André Melliès and Alexis Saurin (looking for connections between non-wellfounded proofs and higher-order automata).

Travaux publiés (ou pas) (Un)published work

Vous pouvez aussi trouver des informations sur vos réseaux sociaux préférés : You can also find some information on your favourite social media: DBLP, ORCID, arXiv.

Journal articles

• J3
  Ohana trees, linear approximation and multi-types for the λI-calculus. No variable gets left behind or forgotten! (under review), with G. Manzonetto and A. Saurin.
  Extended version of [P2].
  AbstractPDFarXiv

  Although the λI-calculus is a natural fragment of the λ-calculus, obtained by forbidding the erasure, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable λI-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the λI-calculus, induced by a notion of evaluation trees that we call “Ohana trees”. The Ohana tree of a λI-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches.

  We develop the associated theories of program approximation: the first approach — more classic — is based on finite trees and continuity, the second adapts Ehrhard and Regnier’s Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a λI-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application.

  Subsequently, we introduce a denotational model designed to capture the equality induced by Ohana trees. Although presented as a non-idempotent type system, our model is based on a suitably modified version of the relational semantics of the λ-calculus, which is known to yield proper models of the λI-calculus when restricted to non-empty finite multisets. To track variables occurring in subterms that are hidden or pushed to infinity in the evaluation trees, we generalize the system in two ways: first, we reintroduce annotated versions of the empty multiset indexed by sets of variables; second, we introduce a separate environment to account for the free variables present in these subterms. We show that this model retains the standard quantitative properties of relational semantics and that the induced theory precisely captures Ohana trees.

  We conclude by discussing the cases of Lévy-Longo and Berarducci trees, and possible generalizations to the full λ-calculus.

• J2
  How to play the Accordion. Uniformity and the (non-)conservativity of the linear approximation of the λ-calculus (under review), with Lionel Vaux Auclair.
  Extended and improved version of [P1].
  AbstractPDFarXiv

  Twenty years after its introduction by Ehrhard and Regnier, differentiation in λ-calculus and in linear logic is now a celebrated tool. In particular, it allows to establish a Taylor expansion formula for various λ-calculi, hence providing a theory of linear approximations for these calculi. In the pure λ-calculus, the linear approximants of λ-terms supporting this Taylor expansion are the terms of a so-called resource calculus, which is equipped with a finitary (strongly normalising) reduction; and the efficiency of this linear approximation is expressed by results stating that the (possibly) infinitary β-reduction of λ-terms is simulated by the reduction of their Taylor expansions, which is induced by the iterated reduction of resource terms. In terms of rewriting systems, resource reduction (operating on infinite linear combinations of Taylor approximants) is an extension of β-reduction.

  In this article, we address the converse property, conservativity: do all reductions between Taylor expansions arise from actual β-reductions? We show that if we restrict the setting to finite terms and β-reduction sequences, then the linear approximation is conservative. However, as soon as one allows infinitary reduction sequences this property is broken. We design a counter-example, the Accordion. Then we show how restricting the reduction of the Taylor approximants allows to build a conservative extension of the β-reduction preserving good simulation properties; this restriction relies on uniformity, a property that was already at the core of Ehrhard and Regnier's pioneering work. Finally, we extend our work to β\(\bot\)-reductions, which play a key role in λ-calculus as they relate a λ-term to its Böhm tree.

• J1
  Finitary Simulation of Infinitary β-Reduction via Taylor Expansion, and Applications (2023), with L. Vaux Auclair.
  Logical Methods in Computer Science, Vol. 19, no. 4. DOI: 10.46298/LMCS-19(4:34)2023.
  AbstractPDFarXiv

  Originating in Girard's Linear logic, Ehrhard and Regnier's Taylor expansion of λ-terms has been broadly used as a tool to approximate the terms of several variants of the λ-calculus. Many results arise from a Commutation theorem relating the normal form of the Taylor expansion of a term to its Böhm tree. This led us to consider extending this formalism to the infinitary λ-calculus, since the \(\Lambda_{\infty}^{001}\) version of this calculus has Böhm trees as normal forms and seems to be the ideal framework to reformulate the Commutation theorem.

  We give a (co-)inductive presentation of \(\Lambda_{\infty}^{001}\). We define a Taylor expansion on this calculus, and state that the infinitary β-reduction can be simulated through this Taylor expansion. The target language is the usual resource calculus, and in particular the resource reduction remains finite, confluent and terminating. Finally, we state the generalised Commutation theorem and use our results to provide simple proofs of some normalisation and confluence properties in the infinitary λ-calculus.

Articles in peer-reviewed proceedings

• P4
  Compression for Coinductive Infinitary Rewriting: A Generic Approach, with Applications to Cut-Elimination for Non-Wellfounded Proofs (under review), with Alexis Saurin.
  AbstractPDFarXiv

  Infinitary rewriting, i.e. rewriting featuring possibly infinite terms and sequences of reduction, is a convenient framework for describing the dynamics of non-terminating but productive rewriting systems. In its original definition based on metric convergence of ordinal-indexed sequences of rewriting steps, a highly desirable property of an infinitary rewriting system is Compression, i.e. the fact that rewriting sequences of arbitrary ordinal length can always be ‘compressed’ to equivalent sequences of length at most ω.

  Since then, the standard examples of infinitary rewriting systems have been given another equivalent presentation based on coinduction. In this work, we extend this presentation to the rewriting of arbitrary non-wellfounded derivations and we investigate compression in this setting. We design a generic proof of compression, relying on a characterisation factorising most of the proof and identifying the key property a compressible infinitary rewriting system should enjoy.

  As running examples, we discuss first-order rewriting and infinitary λ-calculi. For the latter, compression can in particular be seen as a justification of its coinductive presentation in the literature. As a more advanced example, we also address compression of cut-elimination sequences in the non-wellfounded proof system μMALL∞ for multiplicative-additive linear logics with fixed points, which is a key lemma of several cut-elimination results for similar proof systems.

• P3
  Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary λ-Calculi. A fanfiction on [KPSdV'13] (2025).
  Proceedings of the Twelfth Workshop on Fixed Points in Computer Science (FICS 2024), EPTCS 435. See Chapter 1 of my thesis for a longer version. DOI: 10.4204/EPTCS.435.5.
  AbstractPDFarXiv

  Ten years ago, it was shown that nominal techniques can be used to design coalgebraic data types with variable binding, so that α-equivalence classes of infinitary terms are directly endowed with a corecursion principle. We introduce “mixed” binding signatures, as well as the corresponding type of mixed inductive-coinductive terms. We extend the aforementioned work to this setting. In particular, this allows for a nominal description of the sets \(\Lambda^{abc}\) of \(abc\)-infinitary λ-terms (for \(a,b,c \in \{0,1\}\)) and of capture-avoiding substitution on α-equivalence classes of such terms.

• P2
  Ohana trees and Taylor expansion for the λI-calculus. No variable gets left behind or forgotten! (2025), with G. Manzonetto and A. Saurin.
  10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025), LIPIcs vol. 337. Read the extended version [J3] instead. DOI: 10.4230/LIPIcs.FSCD.2025.12.
  AbstractPDFarXiv

  Although the λI-calculus is a natural fragment of the λ-calculus, obtained by forbidding the erasure, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable λI-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the λI-calculus, induced by a notion of evaluation trees that we call ‘Ohana trees’. The Ohana tree of a λI-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches.

  We develop the associated theories of program approximation: the first approach—more classic—is based on finite trees and continuity, the second adapts Ehrhard and Regnier’s Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a λI-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. We conclude by discussing the cases of Lévy-Longo and Berarducci trees, and generalizations to the full λ-calculus.

• P1
  How to play the Accordion. Uniformity and the (non-)conservativity of the linear approximation of the λ-calculus (2025), with L. Vaux Auclair.
  42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025), LIPIcs vol. 327. Read the extended version [J2] instead. DOI: 10.4230/LIPIcs.STACS.2025.23.
  AbstractPDFarXiv

  Twenty years after its introduction by Ehrhard and Regnier, differentiation in λ-calculus and in linear logic is now a celebrated tool. In particular, it allows to write the Taylor formula in various λ-calculi, hence providing a theory of linear approximations for these calculi. In the standard λ-calculus, this linear approximation is expressed by results stating that the (possibly) infinitary β-reduction of λ-terms is simulated by the reduction of their Taylor expansion: in terms of rewriting systems, the resource reduction (operating on Taylor approximants) is an extension of the β-reduction.

  In this paper, we address the converse property, conservativity: are there reductions of the Taylor approximants that do not arise from an actual β-reduction of the approximated term? We show that if we restrict the setting to finite terms and β-reduction sequences, then the linear approximation is conservative. However, as soon as one allows infinitary reduction sequences this property is broken. We design a counter-example, the Accordion. Then we show how restricting the reduction of the Taylor approximants allows to build a conservative extension of the β-reduction preserving good simulation properties. This restriction relies on uniformity, a property that was already at the core of Ehrhard and Regnier's pioneering work.

Other unpublished work

• U2
  The lazy evaluation of the λ-calculus enjoys linear approximation, and that’s all (2025).
  Abstract presented to the 9th International Workshop on Trends in Linear Logic and Interactions (TLLA 2025).
  AbstractPDF

  The advent of a linear approximation of the λ-calculus based on Taylor expansion allowed for a renewal and a refinement of the classic approach based on continuous approximation. The major property of the linear approximation, known as the Commutation theorem, relates the infinitary head normalisation of a λ-term towards its Böhm tree to the (finitary) normalisation of its Taylor expansion, that is, the sum of its multilinear approximants. This approximation theory is therefore related to the standard evaluation of λ-terms, that retains head normal forms as meaningful prefixes of information ; in this work, we adapt it to the lazy evaluation where weak head normal forms play this role. We introduce a lazy resource λ-calculus and the corresponding Taylor expansion, and show that it simulates the 101-infinitary λ-calculus. In particular, we obtain a Commutation theorem with respect to Lévy-Longo trees. This shows that a second normal form model enjoys a linear approximation, out of the \(2^c\) existing normal form models (where \(c\) is the cardinality of the continuum). We conclude by noticing that there cannot be such a linear approximation for all other such models, and in particular for Berarducci trees.

• U1
  Compression for Coinductive Infinitary Rewriting (A Preliminary Account) (2025), with Alexis Saurin.
  Abstract presented to the 12th International Workshop on Higher-Order Rewriting (HOR 2025). Read the real paper [P3] instead.
  AbstractPDF

  In “traditional” infinitary rewriting based on ordinal-indexed rewriting sequences and strong Cauchy convergence, a key property of rewriting systems is compression, that is, the fact that rewriting sequences of arbitrary ordinal length can be compressed to sequences of length ω. Famous examples of compressible systems are left-linear first-order systems and infinitary λ-calculi. In this work, we investigate compression in the equivalent setting of coinductive infinitary rewriting, which we recall in a slightly augmented form: we extend it to rewriting of (possibly non-wellfounded) derivations in an arbitrary sytem of derivation rules. Then we define the coinductive counterpart of compressed rewriting sequences, and we present a general coinductive procedure turning arbitrary infinitary rewriting derivations into compressed ones, without relying on convergence. The coinductive presentation of the two aforementioned examples are endowed with compression lemmas as instances of our general method.

Theses

• T1
  Taylor Approximation and Infinitary λ-Calculi (2024).
  PhD thesis. Under the supervision of L. Vaux Auclair et L. Regnier.
  AbstractPDFHAL

  Since its introduction by Church, the λ-calculus has played a major role in a century of development in theoretical computer science and mathematical logic, as well as in the birth of numerous programming languages. A crucial property of this calculus is that it is not normalising in general, leading to growing interest in finding approximations to its dynamics. The “classic” approximation tools, which emerged in the 1970s in the wake of Scott's semantics, are essentially semantic. The tools based on Taylor expansion, introduced in the 2000s by Ehrhard and Regnier, conversely propose a dynamic approximation of the β-reduction. Drawing its inspiration from the development of linear logic, Taylor expansion translates the λ-calculus into a multilinear “resource” calculus, equipped with finitary dynamics. A commutation theorem (between approximation and normalisation) makes this approach particularly effective, and justifies its success. The notion of Böhm tree is central to this line of research. Associated with the idea that normalising terms are not the only computationally meaningful ones, it generalises the notion of normal form by constituting an “infinite normal form”. Understanding the coinductive nature of this object led in the 1990s to the introduction of infinitary λ-calculi. In these calculi, terms and reductions can be infinite and, in the case of the 001-infinitary calculus, the Böhm tree is the notion of infinite normal form (without quotes).

  The idea guiding this thesis is that the 001-infinitary λ-calculus lends itself to a generalisation of the Taylor approximation where, in particular, Böhm trees would be “ordinary citizens”. The approximation of the finite λ-calculus, and in particular its normalisation properties, then becomes a special case of the approximation of the infinitary calculus. This is enabled by the main result of the thesis, which establishes that the dynamics of the resource calculus is able to simulate the infinitary β-reduction via Taylor expansion.

  To arrive at this result, we first make a diversion via an abstract presentation of a “mixed” (inductive and coinductive) higher-order syntax, using a nominal formalism generalising recent work on coalgebraic types with binders. This allows us to formally define coalgebras of α-equivalence classes of infinite λ-terms (Chapter 1). In a second step, we define infinitary λ-calculi using a coinductive presentation, then recall their main properties as well as their connection with classical theories of approximation of the β-reduction (Chapter 2). Then, we present the resource λ-calculus as a special case of a rewriting with sums, and distinguish its qualitative and quantitative flavours (Chapter 3). In a second part devoted to the Taylor approximation itself, we begin by introducing the Taylor expansion of infinitary λ-terms and prove the announced simulation theorem, in its qualitative and quantitative forms. We demonstrate the effectiveness of this theorem by putting it at work, proposing in particular a new confluence proof for the 001-infinitary λ-calculus (Chapter 4). We also consider the conservativity of the simulation property, and demonstrate the surprising existence of a counterexample to this converse property (Chapter 5). Finally, we extend our work to the lazy setting, i.e. the setting related to the 101-infinitary λ-calculus, and we prove a commutation theorem for Lévy-Longo trees (Chapter 6).

Exposés Talks

Sciences sociales Social sciences

Dans une autre vie, j'ai étudié la sociologie et j'ai toujours beaucoup d'intérêt pour ce domaine, même si je manque de temps pour m'y consacrer. Je me suis surtout intéressé à la sociologie de l'enseignement supérieur :

In another life, I studied sociology and law and I still have many interests in these fields, although I lack time to devote to them. My main focus research-wise was on sociology of higher education:

• curricula en mathématiques : définition et transmission de savoirs pratiques par l'enseignement des mathématiques,
• mathematical curricula: the definition and the transmission of practical knowledge through the teaching of mathematics,
• institutions d'élite dans l'enseignement supérieur,
• elite institutions in higher education,
• santé étudiante (santé mentale en particulier),
• student health (in particular mental health),
• élections étudiantes et engagement politique dans l'enseignement supérieur.
• student elections and political engagement in higher education.

Voici une liste de mes travaux écrits dans ce domaine.

Here is a list of my written work in this domain.

• C1
  Pêcher des poissons pour leur apprendre à nager ? II. En « colles », les mathématiques au service d'une formation élitiste (2023).
  In P.-M. Menger, P. Verschueren (dir.), Le Monde des mathématiques, éd. du Seuil (actes du colloque « Mathématiques, communautés et institutions », Collège de France, 2020).
  AbstractPDFURL

  L'importance persistante des mathématiques dans l'accès à une grande part des filières d'élite en France pousse à s'interroger sur le rôle concret joué par cette discipline et ses cadres d'enseignement dans la (re)production d'une « jeunesse dominante ». Étudiant dans trois lycées prestigieux les « colles » de mathématiques, interrogations orales au cœur du dispositif pédagogique des classes préparatoires, nous montrons que l'apprentissage et l'évaluation des savoirs y sont le support d'une prise en charge institutionnelle des élèves (au moins autant que l'inverse) visant à leur transmettre des dispositions qui excèdent largement le seul cadre des mathématiques. La structure des jugements mathématiques des interrogateurs fait apparaître une valeur d'autonomie, nourrie de la dualité rigueur/intuition classique en mathématiques, qui renouvelle l'idéologie du don bourdieusienne et interfère avec le passé social des élèves — au risque d'agir en différenciant leurs trajectoires.

• T1
  Coller en mathématiques. Rite disciplinaire et formation des élites (2019).
  First year Master thesis in Social sciences. Under the supervision of E. Picard.