Recherche

Research

Mon principal domaine de recherche est l'informatique théorique : la logique mathématique, la théorie de la programmation et leur rapprochement au travers de la correspondance de Curry-Howard. Vous trouverez ci-dessous une liste de mes papiers et de mes exposés sur ces sujets. En outre, j'ai une formation (modeste) et un intérêt (sous-exploité) dans les domaines de la sociologie et du droit, cf. la section correspondante pour quelques détails.

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.

Mes intérêts initiaux sont la théorie de la démonstration (principalement autour de logiques sous-structurelles, comme la logique linéaire) ainsi que les sémantiques opérationnelle et dénotationnelle du λ-calcul (ou de variantes de celui-ci).

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).

• Dans ma thèse avec Lionel Vaux Auclair, j'ai reformulé l'approximation linéaire des programmes fonctionnels (alias développement de Taylor pour le λ-calcul) à l'aide d'outils de réécriture infinitaire [J1,P2,T1].
• 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 [J1,P2,T1].
• Je travaille actuellement avec Giulio Manzonetto et Alexis Saurin sur un raffinement de cette approximation de programmes et de la sémantique quantitative associée, dans le but de capturer le (non-)effacement de portions de programmes le long de calculs infinis [U1].
• 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 [U1].

Plus généralement, je suis particulièrement intéressé par l'étude d'objets et de processus infinis en informatique, par exemple à l'aide de termes et de réécritures infinitaires, de techniques coinductives, de points fixes.

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.

• Dans le cadre de ma thèse, j'ai travaillé sur une syntaxe nominale pour des termes mixtes inductifs-coinductifs avec lieurs [P1].
• As part of my PhD, I worked on a nominal syntax for mixed inductive-coinductive data types with variable binding [P1].
• Avec Pierre Guillon et Lionel Vaux Auclair, je travail sur certaines propriétés de réécritures infinitaires en dynamique et en calculabilité.
• With Pierre Guillon and Lionel Vaux Auclair, I work on dynamical and computability properties of infinitary rewriting systems.
• En ce moment, je travaille principalement sur des systèmes de preuve non-bien-fondées pour des logiques avec points fixes. En particulier, je cherche à connecter ce formalisme avec les automates d'ordre supérieur et les questions de vérification liées, avec Paul-André Melliès et Alexis Saurin.
• Currently, I'm mainly working on non-wellfounded proof theory for logics with fixed points. In particular, I'm investigating connections of this formalism with higher-order automata and verification, with Paul-André Melliès and Alexis Saurin.

Parmi les autres sujets sur lesquels j'aimerais me pencher : le raisonnement non-bien-fondé dans les assistants de preuve, les logiques/types sous-structurels pour la concurrence, l'approximation de calculs de processus, entre autres.

Among the other topics I'd like to investigate: non-wellfounded reasoning in proof assistants, substructural logics and types for concurrency, approximation of process calculi, and more.

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.

[P2]
• 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. DOI: 10.4230/LIPIcs.STACS.2025.23.
  AbstractPDF

  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.

[U1]
• Memory trees and Taylor expansion for the λI-calculus. No variables left behind, or forgotten! (submitted), with G. Manzonetto and A. Saurin.
  Working title.
  AbstractPDF

  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 ‘memory trees’. The memory 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 memory tree. As a corollary, we obtain that the equality induced by memory 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.

[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).

[P1]
• Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary λ-Calculi. A fanfiction on [KPSdV'13] (to appear).
  To appear in the proceedings of FICS 2024. See Chapter 1 of my thesis for a longer version.
  AbstractPDF

  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.

[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.

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 I still have many interests in this field, although I lack time to devote to it. My main focus is 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.

Je termine aussi une formation de droit. La recherche associant droit et informatique semble ouvrir de nombreuses perspectives : j'adorerais m'impliquer dans ce genre de travaux, n'hésitez pas à me contacter à ce sujet !

I'm also completing a degree in Law. There seem to be many promising lines of research joining law and computer science: I would enjoy getting involved in such work, feel free to contact me about this!