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,T1,P2,U2].
• 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,T1,P2,U2].
• 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 [P3].
• 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 [P3].

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 travaille 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, avec Alexis Saurin j'étudie la réécriture infinitaire de dérivations non-bien-fondées [U1]. Avec Paul-André Melliès, nous cherchons également à connecter ce formalisme avec les automates d'ordre supérieur et les questions de vérification liées.
• Currently, I'm mainly working on non-wellfounded proof theory for logics with fixed points. In particular, I'm investigating infinitary rewriting of non-wellfounded derivations with Alexis Saurin [U1]. With Paul-André Melliès, we also look for connections of this formalism with higher-order automata and verification.

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.

• J2
  How to play the Accordion. Uniformity and the (non-)conservativity of the linear approximation of the λ-calculus (soumis), avec Lionel Vaux Auclair.
  Extended and improved version of [P1].
  RésuméPDF

  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.

• P4
  Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary λ-Calculi. A fanfiction on [KPSdV'13] (2025).
  Actes de FICS 2024, EPTCS 435. Version plus détaillée dans le chapitre 1 de ma thèse. DOI: 10.4204/EPTCS.435.5.
  RésuméPDFarXiv

  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.

• P3
  Compression for Coinductive Infinitary Rewriting: A Generic Approach, with Applications to Cut-Elimination for Non-Wellfounded Proofs (soumis), avec Alexis Saurin.
  RésuméPDFarXiv

  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.

• U2
  The lazy evaluation of the λ-calculus enjoys linear approximation, and that’s all (2025).
  Résumé présenté au 9th International Workshop on Trends in Linear Logic and Interactions (TLLA 2025).
  RésuméPDF

  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), avec Alexis Saurin.
  Résumé présenté au 12th International Workshop on Higher-Order Rewriting (HOR 2025). Lire plutôt le vrai article [P3].
  RésuméPDF

  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.

• P2
  Ohana trees and Taylor expansion for the λI-calculus. No variable gets left behind or forgotten! (2025), avec G. Manzonetto et A. Saurin.
  10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025), LIPIcs vol. 337. DOI: 10.4230/LIPIcs.FSCD.2025.12.
  RésuméPDFarXiv

  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), avec 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.
  RésuméPDF

  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.

• T1
  Taylor Approximation and Infinitary λ-Calculi (2024).
  Thèse de doctorat. Sous la direction de L. Vaux Auclair et L. Regnier.
  RésuméPDFHAL

  Depuis son introduction par Church, le λ-calcul a joué un rôle majeur dans un siècle de développement de l'informatique théorique et de la logique mathématique, mais aussi dans la naissance de nombreux langages de programmation. Une propriété cruciale de ce calcul est qu'il n'est pas normalisant en général, de sorte qu'un intérêt croissant a porté sur la recherche d'approximations de sa dynamique. Les outils « classiques » d'approximation, nés dans les années 1970 dans le sillage des sémantiques de Scott, sont essentiellement sémantiques. Les outils basés sur le développement de Taylor, introduits dans les années 2000 par Ehrhard et Regnier, proposent à l'inverse une approximation dynamique de la β-réduction. Puisant ses inspirations dans le développement de la logique linéaire, le développement de Taylor traduit le λ-calcul vers un calcul « à ressources » multilinéaire, muni d'une dynamique finitaire. Un théorème de commutation (entre approximation et normalisation) fait notamment l'efficacité de cette approche, et en justifie le succès. La notion d'arbre de Böhm est centrale dans cette ligne de recherche. Née de l'idée que les termes normalisants ne sont pas les seuls à avoir un sens calculatoire, elle généralise la notion de forme normale en constituant une «forme normale à l'infini». La compréhension de la nature coinductive de cet objet a mené dans les années 1990 à l'introduction de λ-calculs infinitaires. Dans ces calculs, les termes et les réductions peuvent être infinis et, dans le cas du calcul 001-infinitaire, l'arbre de Böhm est la notion de forme normale à l'infini (sans guillemets).

  L'idée qui guide cette thèse est que le λ-calcul 001-infinitaire se prête à une généralisation de l'approximation de Taylor où, en particulier, les arbres de Böhm seraient des «citoyens ordinaires». L'approximation du λ-calcul fini, et notamment de ses propriétés de normalisation, devient alors un cas particulier de l'approximation du calcul infinitaire. Cela est permis par le principal résultat de la thèse, qui établit que la dynamique du calcul à ressources est à même de simuler la β-réduction infinitaire via le développement de Taylor.

  Pour arriver à ce résultat, nous faisons d'abord un détour par une présentation abstraite d'une syntaxe « mixte » (inductive et coinductive) d'ordre supérieur, à l'aide d'un formalisme nominal généralisant des travaux récents introduisant des types coalgébriques avec lieurs. Cela nous permet de définir formellement des coalgèbres de classes d'α-équivalence de λ-termes infinitaires (chapitre 1). Dans un second temps, nous définissons les λ-calculs infinitaires à l'aide d'une présentation coinductive, puis nous rappelons leurs principales propriétés ainsi que leur lien avec les théories classiques de l'approximation de la β-réduction (chapitre 2). Ensuite, nous présentons le λ-calcul à ressources comme un cas particulier d'une réécriture avec sommes, et distinguons ses versions qualitative et quantitative (chapitre 3). Dans une seconde partie consacrée à l'approximation de Taylor proprement dite, nous commençons par introduire le développement de Taylor des λ-termes infinitaires et prouvons le théorème de simulation annoncé, dans sa forme qualitative puis quantitative. Nous démontrons l'efficacité de ce théorème en le mettant à l'œuvre, proposant notamment une nouvelle preuve de confluence pour le λ-calcul 001-infinitaire (chapitre 4). Nous nous penchons également sur la conservativité de la propriété de simulation, et démontrons l'existence surprenante d'un contre-exemple à cette propriété réciproque (chapitre 5). Enfin, nous étendons notre travail au cadre paresseux, c'est-à-dire celui du λ-calcul 101-infinitaire, et nous démontrons un théorème de commutation pour les arbres de Lévy-Longo (chapitre 6).

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

  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).
  RésuméPDFLien

  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).
  Mémoire de recherche dans le cadre d'un M1 de sciences sociales. Sous la direction d'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!