[[https://www.irif.fr/_media/users/saurin/pub/fossacs2025.pdf|Cut-elimination for the circular modal mu-calculus: linear logic and super exponentials to the rescue]], with Esaïe Bauer, FOSSACS 2025

This paper presents a proof-theoretic analysis of the modal mu-calculus, well-known in verification theory and relevant to the model-checking problem.
More precisely, we prove a syntactic cut-elimination for the non-wellfounded modal mu-calculus, using methods from linear logic and its exponential modalities. To achieve this, we introduce a new system, μLL∞, which is a linear version of the modal mu-calculus, intertwining the modalities from the modal mu-calculus with the exponential modalities from linear logic.
Our strategy for proving cut-elimination involves (i) proving cut-elimination for μLL∞ and (ii) translating proofs of the modal mu-calculus into this new system via a "linear translation", allowing us to extract the cut-elimination result.

* 2023: *

[[https://www.irif.fr/_media/users/saurin/pub/fsttcs2023.pdf|Comparing infinitary systems for linear logic with fixed points]], Anupam Das, Abhishek De & Alexis Saurin, FSTTCS 2023

Extensions of Girard's linear logic by least and greatest fixed point operators (muMALL) have been an active field of research for almost two decades. Various proof systems are known viz. finitary and non-wellfounded, based on explicit and implicit (co)induction respectively.
In this paper, we compare the relative expressivity, at the level of provability, of two complementary infinitary proof systems: finitely branching non-wellfounded proofs (muMALLnwf) vs. infinitely branching well-founded proofs (muMALLomega). Our main result is that muMALLnwf is strictly contained in muMALLomega. An immediate consequence is that muMALLnwf does not enjoy a finite model property in any adequate semantics.
For inclusion, we devise a novel technique involving infinitary rewriting of non-wellfounded proofs that gives a wellfounded proof in the limit. For strictness of the inclusion, we improve previously known lower bounds on muMALLnwf provability, from \Pi^0_1-hard to \Sigma^1_1-hard, by encoding a sort of Buchi condition for Minsky machines.

[[https://link.springer.com/chapter/10.1007/978-3-031-43513-3_12|A Linear Perspective on Cut-Elimination for Non-wellfounded Sequent Calculi with Least and Greatest Fixed-Points]], Alexis Saurin, TABLEAUX 2023 (A long version is [[https://hal.science/hal-04169137|accessible on hal]])

This paper establishes cut-elimination for μLL∞, μLK∞ and μLJ∞, that are non-wellfounded sequent calculi with least and greatest fixed-points, by expanding on prior works by Santocanale and Fortier [20] as well as Baelde et al. [3, 4].
The paper studies a fixed-point encoding of LL exponentials in order to deduce those cut-elimination results from that of μMALL∞.
Cut-elimination for μLK∞ and μLJ∞ is obtained by developing appropriate linear decorations for those logics.

[[https://arxiv.org/abs/2310.09038|On the exponential logic of sequentialization]], Aurore Alcolei, Luc Pellissier & Alexis Saurin, MFPS 2023

Linear logic has provided new perspectives on proof-theory, denotational semantics and the study of programming languages. One of its main successes are proof-nets, canonical representations of proofs that lie at the intersection between logic and graph theory. In the case of the minimalist proof-system of multiplicative linear logic without units (MLL), these two aspects are completely fused: proof-nets for this system are graphs satisfying a correctness criterion that can be fully expressed in the language of graphs. For more expressive logical systems (containing logical constants, quantifiers and exponential modalities), this is not completely the case. The purely graphical approach of proof-nets deprives them of any sequential structure that is crucial to represent the order in which arguments are presented, which is necessary for these extensions. Rebuilding this order of presentation - sequentializing the graph - is thus a requirement for a graph to be logical. Presentations and study of the artifacts ensuring that sequentialization can be done, such as boxes or jumps, are an integral part of researches on linear logic. Jumps, extensively studied by Faggian and di Giamberardino, can express intermediate degrees of sequentialization between a sequent calculus proof and a fully desequentialized proof-net. We propose to analyze the logical strength of jumps by internalizing them in an extention of MLL where axioms on a specific formula, the jumping formula, introduce constrains on the possible sequentializations. The jumping formula needs to be treated non-linearly, which we do either axiomatically, or by embedding it in a very controlled fragment of multiplicative-exponential linear logic, uncovering the exponential logic of sequentialization.

[[https://drops.dagstuhl.de/opus/volltexte/2023/17474/|A Curry-Howard Correspondence for Linear, Reversible Computation]], Kostia Chardonnet, Alexis Saurin & Benoît Valiron, CSL 2023

In this paper, we present a linear and reversible programming language with inductives types and recursion. The semantics of the languages is based on pattern-matching; we show how ensuring syntactical exhaustivity and non-overlapping of clauses is enough to ensure reversibility. The language allows to represent any Primitive Recursive Function. We then give a Curry-Howard correspondence with the logic μMALL: linear logic extended with least fixed points allowing inductive statements. The critical part of our work is to show how primitive recursion yields circular proofs that satisfy μMALL validity criterion and how the language simulates the cut-elimination procedure of μMALL.

* 2022 *

[[https://drops.dagstuhl.de/opus/volltexte/2022/17427/|Phase semantics for linear logic with least and greatest fixed-points]], Abhishek De, Farzad Jafarrahmani & Alexis Saurin, FSTTCS 2022

The truth semantics of linear logic (i.e. phase semantics) is often overlooked despite having a wide range of applications and deep connections with several denotational semantics. In phase semantics, one is concerned about the provability of formulas rather than the contents of their proofs (or refutations). Linear logic equipped with the least and greatest fixpoint operators (µMALL) has been an active field of research for the past one and a half decades. Various proof systems are known viz. finitary and non-wellfounded, based on explicit and implicit (co)induction respectively.
In this paper, we extend the phase semantics of multiplicative additive linear logic (a.k.a. MALL) to µMALL with explicit (co)induction (i.e. µMALL ind). We introduce a Tait-style system for µMALL called µMALLω where proofs are wellfounded but potentially infinitely branching. We study its phase semantics and prove that it does not have the finite model property.

[[https://drops.dagstuhl.de/opus/volltexte/2022/16301/|Decision Problems for Linear Logic with Least and Greatest Fixed Points]], Anupam Das, Abhishek De & Alexis Saurin, FSCD 2022

Linear logic is an important logic for modelling resources and decomposing computational interpretations of proofs. Decision problems for fragments of linear logic exhibiting "infinitary" behaviour (such as exponentials) are notoriously complicated. In this work, we address the decision problems for variations of linear logic with fixed points (μMALL), in particular, recent systems based on "circular" and "non-wellfounded" reasoning. In this paper, we show that μMALL is undecidable.
More explicitly, we show that the general non-wellfounded system is Π⁰₁-hard via a reduction to the non-halting of Minsky machines, and thus is strictly stronger than its circular counterpart (which is in Σ⁰₁). Moreover, we show that the restriction of these systems to theorems with only the least fixed points is already Σ⁰₁-complete via a reduction to the reachability problem of alternating vector addition systems with states. This implies that both the circular system and the finitary system (with explicit (co)induction) are Σ⁰₁-complete.

[[https://dl.acm.org/doi/10.1145/3531130.3533375|Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs]], David Baelde, Amina Doumane, Denis Kuperberg & Alexis Saurin, LICS 2022 (see the [[https://hal.science/hal-03682126|open-access extended version on hal]])

Given that (co)inductive types are naturally modelled as fixed points, it is unsurprising that fixed-point logics are of interest in the study of programming languages, via the Curry-Howard (or proofs-as-programs) correspondence. This motivates investigations of the structural proof-theory of fixed-point logics and of their cut-elimination procedures.
Among the various approaches to proofs in fixed-point logics, circular – or cyclic – proofs, are of interest in this regard but suffer from a number of limitations, most notably from a quite restricted use of cuts. Indeed, the validity condition which ensures soundness of non-wellfounded derivations and productivity of their cut-elimination prevents some computationally-relevant patterns of cuts. As a result, traditional circular proofs cannot serve as a basis for a theory of (co)recursive programming by lack of compositionality: there are not enough circular proofs and they compose badly.
The present paper addresses some of these limitations by developing the circular and non-wellfounded proof-theory of multiplicative additive linear logic with fixed points (μMALL∞) beyond the scope of the seminal works of Santocanale and Fortier and of Baelde et al. We define bouncing-validity: a new, generalized, validity criterion for μMALL∞, which takes axioms and cuts into account. We show soundness and cut elimination theorems for bouncing-valid non-wellfounded proofs: as a result, even though bouncing-validity proves the same sequents (or judgments) as before, we have many more valid proofs at our disposal. We illustrate the computational relevance of bouncing-validity on a number of examples. Finally, we study the decidability of the criterion in the circular case: we prove that it is undecidable in general but identify a hierarchy of decidable sub-criteria.

* Before 2022: You can find [[https://dblp.org/pid/19/1889.html|my publications before 2022 on DBLP]]. == Open-access and drafts == Here are some drafts and open-access publications: * [[https://www.irif.fr/_media/users/saurin/pub/interpolation_as_cut_introduction.pdf|Interpolation as Cut-Introduction]], draft February 2024, updated in March 2025

After Craig and Lyndon's seminal results on interpolation theorem, a number and variety of proof-techniques, be they semantical or proof-theoretical, have been designed to prove interpolation theorems. Among them, Maheara's method is quite specific by its general applicability to logic admitting cut-free complete proof systems.
In the present paper, we reconsider Maehara's method and show that, by a close inspection of the proof, one can extract a "proof-relevant" interpolation theorem for first-order linear-logic which can stated as follows: if π proves A ⊢ B, we can find (i) a formula C in the common vocabulary of A and B and (ii) proofs π1, π2 of A ⊢ C and C ⊢ B respectively such that the proof π' obtained by composing π1 with π2 (that is the proof of A ⊢ B built with a cut inference of premises π1 and π2) is cut-equivalent to π. This result is (easily) extended to classical and intuitionistic logics (thanks to linear translations) and sheds an interesting light on the relationship between Lyndon and Craig's interpolation.
Interpolation can therefore be achieved while preserving the computational content of proofs. After discussing the computational interpretation of our interpolation theorem as well as related results in natural deduction (based on Prawitz' proof of interpolation), we consider two extensions.
First, by a further analysis of Maehara's method, we show that the interpolation process for a cut-free proof π deriving A ⊢ B can be in fact decomposed in two phases: (i) an ascending phase which equips each sequent of π with a partition is followed by (ii) a descending phase which solves the interpolation problem. This latter descending phase happens to be a cut-introduction phase providing an alternative proof of our proof-relevant interpolation result. The resulting proof is, by construction, denotationally equal to π. This is carried out through the notion of proof-relevant interpolation situation (PRIS) which allows to structure nicely the construction. We also consider what happens if proofs are not cut-free.
Then, we consider the question of extending our approach to the mu-calculus and non-wellfounded proofs. We show that, for circular pre-proofs (disregarding the validity condition), the method extends smoothly and discuss a roadmap to take validity into account.
Finally, we turn to the computational analysis of the result, showing how our proof-relevant inteprolation method can be performed in System L, a term calculus in the vein of the Curien-Herbelin so-called duality of computation where terms, which are close to states of an abstract machines, can be put in correspondence with sequent claculus derivation. We carry out the result in the multiplicative and additive case of linear logic but the same results can be obtained for the classical calculus as well; straightforwardly following the same path.

* [[https://www.irif.fr/_media/users/saurin/pub/musuperll-and-cut-elimination.pdf|A uniform cut-elimination theorem for linear logics with fixed points and super-exponentials]] with Esaïe Bauer, March 2025

In the realm of light logics deriving from linear logic, a number of variants of exponential rules have been investigated. The profusion of such proof systems induce the need for cut-elimination theorems for each logic the proof of which may be redundant. A number of approaches in proof theory have been adopted to cope with this need. In the present paper, we consider this issue from the point of view of enhancing linear logic with least and greatest fixed-points and considering such a variety of exponential connectives.
Our main contribution is to provide a uniform cut-elimination theorem for a parametrized system with fixed-points by combining two approaches: cut-elimination proofs by reduction (or translation) to another system and the identification of sufficient conditions for cut-elimination. More precisely, we examine a broad range of systems, building on Nigam and Miller’s subexponentials and Bauer and Laurent’s super exponentials. Our work is motivated by our recent work on cut-elimination for the modal μ-calculus as well as by Baillot’s work on light logics with recursive types.

* [[https://www.irif.fr/_media/users/saurin/ohana-trees.pdf|Memory trees and Taylor expansion for the λI-calculus -- No variables left behind or forgotten!]] with Rémy Cerda and Giulio Manzonetto, March 2025

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.

[[https://arxiv.org/pdf/2302.11887|A Curry-Howard Correspondence for Linear, Reversible Computation]], with Kostia Chardonnet and Benoît Valiron, draft, version of january 2025

[[https://www.irif.fr/_media/users/saurin/pub/nwf-circ-denot-2024.pdf|On denotations of circular and non-wellfounded proofs]], with Thomas Ehrhard &Farzad Jafarrahmani, draft, version of january 2024

This paper investigates the question of denotational invariants of non-wellfounded and circular proofs of the linear logic with least and greatest fixed-points. Indeed, while non-wellfounded and circular proof theory made significant progress in the last twenty years, the corresponding denotational semantics is still underdeveloped.
A denotational semantics for non-wellfounded proofs, based on a notion of totality, is provided, building on previous work by Ehrhard and Jafarrahmani. Several properties of the semantics are then studied: its soundness, the relation between totality and validity and the semantical content of the translation from finitary proofs to circular proofs. Finally, the paper focuses on circular proofs, trying to benefit from their regularity in order to define inductively the interpretation function. It is argued why the usual validity condition is too general for that purpose, while a fragment of circular proofs, strongly valid proofs, constitutes a well-behaved class for such an inductive interpretation.

[[https://www.irif.fr/_media/users/saurin/pub/cut_elim_modal_draft.pdf|Cut-elimination for the circular modal mu-calculus: linear logic and super exponentials to the rescue]], with Esaïe Bauer, draft, version of january 2024
*

[[https://hal.science/hal-03655737v1|Polarized linear logic with fixpoints]], with Thomas Ehrhard & Farzad Jafarrahmani, draft 2022

We introduce and study µLLP, which can be viewed both as an extension of Laurent's Polarized Linear Logic, LLP, with least and greatest fixpoints, and as a polarized version of Baelde's Linear Logic with fixpoints (µMALL and µLL). We take advantage of the implicit structural rules of µLLP to introduce a term syntax for this language, in the spirit of the classical lambda-calculus and of system L in the style of Curien, Herbelin and Munch-Maccagnoni. We equip this language with a deterministic reduction semantics as well as a denotational semantics based on the notion of non-uniform totality spaces and the notion of categorical model for linear logic with fixpoint introduced by Ehrhard and Jafarrahmani. We prove an adequacy result for µLLP between these operational and denotational semantics, from which we derive a normalization property for µLLP thanks to the properties of the totality interpretation.

==== Teaching ==== During the fall semester 2024-2025, I have been teaching at Master LMFI (second year master in mathematical logic and foundations of computer science) at Université Paris Cité. * [[https://www.irif.fr/users/saurin/teaching/lmfi/coq-2024/index|Course on functional programming and formal proofs in Coq (PF2)]] /* * [[https://www.irif.fr/users/saurin/teaching/lmfi/coq-2023|Course on functional programming and formal proofs in Coq (PF2)]] */ During the second semester 2023-24, I was teaching with Thomas Colcombet the course on * [[https://www.irif.fr/users/saurin/teaching/lmfi/sofix-2024|Second-order quantification and fixed points in logic (SOFIX)]] In the previous years, I have mostly been teaching in M2 LMFI (Cours fondamental de logique-théorie de la démonstration; Outils classiques pour la corespondance preuves-programmes; logique linéaire; lambda-calcul et preuves) but also in the Programming M2 (computer labs in the course of Adrien Guatto on synchronous programming) or in L1 (IP1, which is the first introductory course on programming for undergraduate studients). I also taught in Centre pénitentiaire de Fresnes and Maison d'arrêt de Paris la Santé as a member of the teaching staff of //Section des étudiants empêchés// and I organized some "math club" in the above two prisons well as in Centre pénitentiaire sud-francilien (in the QCD of Réau). Most of my teaching activities were in fact part of voluntary social work as a member of GENEPI (including one year of "civil service" during my PhD studies where I lead this student NGO which does not exist anymore) when I was a student and then as a volunteer in FARAPEJ, in Mathématiques en liberté, and in Champ Libre. ==== Students and post-docs ==== == Current PhD student: == * [[https://www.irif.fr/users/ebauer/index|Esaïe Bauer]] == Current Post-doctoral fellow: == * [[https://www.i2m.univ-amu.fr/perso/remy.cerda/|Rémy Cerda]] == Former PhD students: == * Farzad Jafarrahmani ([[https://www.theses.fr/s230580|defended january 2023]], co-advised with Thomas Ehrhard), currently post-doc in LIP6 ([[https://drive.google.com/file/d/1o9kLi14VDjRb1N2TTfF1WzwG5e25N1xK/view?usp=sharing|manuscript]], [[https://sites.google.com/site/farzadjafarrahmani/|webpage]]) * Kostia Chardonnet ([[https://www.theses.fr/2023UPASG005|defended january 2023]], co-advised with Benoît Valiron), currently post-doc in Bologna ([[https://www.theses.fr/2023UPASG005|manuscript]], [[https://www.lri.fr/~chardonnet/|webpage]]) * Abhishek De ([[https://www.theses.fr/2022UNIP7128|defended december 2022]]), currently post-doc in Birmingham ([[https://www.theses.fr/2022UNIP7128|manuscript]]) * Rémi Nollet (defended summer 2021, co-advised with Christine Tasson), professeur de CPGE ([[https://theses.fr/2021UNIP7100|manuscrit]]) * Amina Doumane ([[https://www.theses.fr/2017USPCC123|defended june 2017]], co-advised with David Baelde), CNRS researcher ([[https://www.theses.fr/2017USPCC123|manuscript]], [[https://perso.ens-lyon.fr/amina.doumane/|webpage]]) * Pierre-Marie Pédrot ([[https://www.theses.fr/2015USPCC240|defended september 2015]], co-advised with Hugo Herbelin), INRIA researcher ([[https://www.pédrot.fr/articles/thesis.pdf|manuscript]], [[https://www.pédrot.fr|webpage]]) == Former Post-doc: == * Aurore Alcoléi (jan 2022 - june 2023) * Luc Pellissier (dec 2018 - dec 2019) * Andrew Polonsky (jan 2016 - december 2017) * Guilhem Jaber (dec 2015 - dec 2016) == Former Master and Undergrad Students: == Guido Fiorillo, Daniel Osorio, Erin Le Boulc'h, Adrien Shalit, Amel Kebbouche Esaïe Bauer, Ikram Cherrigui, Naïm Favier, Lucien David, Kostia Chardonnet, Rémi Nollet, Pablo Donato, Xavier Onfroy, Paul Fermé, Amina Doumane, Paul Downen, Fanny Hé, Simon Lunel, Luke Maurer ==== Contact informations ==== {{page>inc&noheader&nofooter}}