Alexis Saurin

Introduction / Research interests / News / Publications and drafts / Teaching / Students and post-docs / Contact informations

I am a CNRS researcher working in Informatique Mathématique (mathematical computer science) at IRIF (Institut de Recherche en Informatique fondamentale), member of PPS pole and Picube Inria team.

I am in charge, together with Esaïe Bauer, of the Formath seminar, which is the seminar of Picube INRIA team. I am also responsible, with Pierre Clairambault and Chantal Keller, of chairing the Scalp working group of GDR-IM and organizing its annual meetings. I am the PI of the ANR funded collaborative project RECIPROG.

I am an elected member of the research council and the academic council of the faculty of Science at Université Paris Cité and an appointed member at the research council of the faculty of Society and Humanity.

My research interests are at the interplay between structural proof theory and the theory of programming, both from a syntactical and semantical perspective. More precisely, I am currently interested in:

• logic and computation: structural proof theory & theory of programming, curry-howard correspondence
• fixed points in logic and programming
• circular and non-wellfounded proofs: proof-theory of the mu-calculus
• linear logic and computational interpretations of classical and intuitionistic logics
• type theory and in particular inductive and coinductive types
• interactive theorem proving
• proof nets and the logic of correctness criteria
• interactive and denotational semantics of proofs and programs
• lambda-calculus and its classical and infinitary extensions
• focusing & multifocusing
• interpolation theorems

• mar 24: seminar at I2M
• oct 23: I am organizing FICS workshop in february 2024;
• sep 23: I am organizing the 2023 annual meeting of SCALP working group, on 27-29 november in Orléans;
• sep 23: In september 2023, I presented my recent paper on cut-elimination for full non-wellfounded linear logic with fixed-points published in TABLEAU 23. A long version is accessible here;
• jul 23: I recently gave an invited tutorial at TLLA 2023 in Rome;
• jul 23: the election for central councils at Uiversité Paris Cité took place during the Spring. PUPH won the elections in the faculties of Science as well as Society and Humanity. Congrats to all those who made it possible, especially Claire Saillard, Maximilien Cazayous and Gaël Mahé!
• jun 23: Aurore Alcolei presented at MFPS 2023 our joint paper with Luc Pellissier on a logical understanding of jumps in MLL proof nets;
• jun 23: Adrien Shalit started his LMFI M2 internship aiming at studying LL observational equivalence through the fixed-point encoding on the exponentials, supervised by Daniela Petrisan and me;
• may 23: I gave a talk at PPS days, in Paris: “What is the (fixed-)point of LL exponentials?”;
• apr 23: JNIM 2023 took place in Université Paris Cité, organized by Marie Albenque, Marie Fortin, Mikaël Rabie and Arnaud Sangnier. Due to strikes and proptests, we decided to cancel the thematic session that we organized on proof assistants. Hopefully it will be reschedulled next year at JNIM 2024!
• mar 23: Finally, we organized Scalp 2022 annual meeting early 2023! It took place at CIRM in february and the scientific program and slides of talks are available online. It took place during the protests about the pension reform by the government and was the occasion for us to initiate a time for social and political discussion during our annual meeting (read here, in french), a practice we aim at pursuing during future.
• feb 23: Kostia Chardonnet presented at CSL 2003 our joint paper with Benoît Valiron on type isomorphisms in MALL with fixed-points as a reversible programming language;
• dec 22: Abhishek De presented at FSTTCS 2022 our joint paper with Farzad Jaffarahmani on phase semantics for linear logic with fixed-points;
• aug 22: Abhishek De presented at FSCD 2022 our joint paper with Abhishek De on complexity of provability in linar logic with fixed-poins;
• aug 22: David Baelde presented at LICS 2022, during FLOC 2022, our joint paper with Amina Doumane and Denis Kuperberg, on circular proofs with Bouncing threads. An preprint of the extended version is available on HAL;
• jun 22: I gave an invited talk at the special session on logic in computer science, at Logic colloquium june 2022;
• may 22: I gave an invited talk at Strip workshop, in Birmingham, may 2022, organized by Anupam Das;
• nov 21: I gave a talk at the Proof Theory Virtual Seminar entitled Virtuous circles in proofs. You can even find a video on the website of the PTVS.

You can find an updated list of my publications on DBLP.

• 2023:
  • 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.
  • 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 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.
  • 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.
  • 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
  • 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.
  • 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.
  • 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 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 my publications before 2022 on DBLP.

Here are some drafts and open-access publications:

• Interpolation as Cut-Introduction, draft February 2024
  

  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 π.
  Finally, 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.
• 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.
• 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
  

  The aim of this paper is twofold: contributing to the non-wellfounded and circular proof-theory of the modal mu-calculus and to that of extensions of linear logic with fixed points. Contrarily to Girard’s linear logic which is equipped with a rich proof theory, Kozen’s modal mu-calculus has an underdeveloped one: for instance the modal mu-calculus is lacking a proper syntactic cut-elimination theorem.
  A strategy to prove the cut-elimination theorem for the modal mu-calculus is to prove cut-elimination for a "linear translation" of the modal mu-calculus (that is define a translation of the statements and proofs of the modal mu-calculus into a linear sequent calculus) and to deduce the desired cut-elimination results as corollaries. While designing this linear translation, we come up with a sequent calculus exhibiting several modalities (or exponentials). It happens that the literature of linear logic offers tools to manage such calculi, for instance subexponentials by Nigam and Miller and superexponentials by Bauer and Laurent.
  We actually extend super exponentials with fixed-points and non-wellfounded proofs (of which the linear decomposition of the modal mu-calculus is an instance) and prove a syntactic cut- elimination theorem for these sequent calculi in the framework of non-wellfounded proof theory. Back to the classical modal mu- calculus, we deduce its cut-elimination theorem from the above results, investigating both non-wellfounded and regular proofs.
• 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.

During the fall semester 2023-24, I have been teaching at Master LMFI (second year master in mathematical logic and foundations of computer science) at Université Paris Cité.

• Course on functional programming and formal proofs in Coq (PF2)

During the second semester 2023-24, I am teaching with Thomas Colcombet the course on

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

• Esaïe Bauer

• Farzad Jafarrahmani (defended january 2023, co-advised with Thomas Ehrhard), currently post-doc in LIP6 (manuscript, webpage)
• Kostia Chardonnet (defended january 2023, co-advised with Benoît Valiron), currently post-doc in Bologna (manuscript, webpage)
• Abhishek De (defended december 2022), currently post-doc in Birmingham (manuscript)
• Rémi Nollet (defended summer 2021, co-advised with Christine Tasson), professeur de CPGE (manuscrit)
• Amina Doumane (defended june 2017, co-advised with David Baelde), CNRS researcher (manuscript, webpage)
• Pierre-Marie Pédrot (defended september 2015, co-advised with Hugo Herbelin), INRIA researcher (manuscript, webpage)

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

Adrien Shalit, Esaïe Bauer, Ikram Cherrigui, Lucien David, Kostia Chardonnet, Rémi Nollet, Pablo Donato, Xavier Onfroy, Paul Fermé, Amina Doumane, Paul Downen, Fanny Hé, Simon Lunel, Luke Maurer