====== Alexis Saurin ======

<wrap right>**[[#introduction|Introduction]]
/ [[#research_interests|Research interests]]
/ [[#news|News]]
/ [[#publications_and_drafts|Publications and drafts]]
/ [[#teaching|Teaching]]
/ [[#students_and_post-docs|Students and post-docs]]
/ [[#contact_informations|Contact informations]]**
</wrap>



/*
  * <wrap em right>[[#introduction|Introduction]]</wrap>
  * <wrap em right>[[#research_interests|Research interests]]</wrap>
  * <wrap em right>[[#news|News]]</wrap>
  * <wrap em right>[[#publications_and_drafts|Publications and drafts]]</wrap>
  * <wrap em right>[[#teaching|Teaching]]</wrap>
  * <wrap em right>[[#students_and_post-docs|Students and post-docs]]</wrap>
  * <wrap em right>[[#contact_informations|Contact informations]]</wrap>
*/

==== Introduction ====

I am a CNRS researcher working in Informatique Mathématique (mathematical computer science) at IRIF (Institut de Recherche en Informatique fondamentale), member of [[https://www.irif.fr/poles/pps/index|PPS pole]] and [[https://www.irif.fr/equipes/picube/index|Picube Inria team]].

I am in charge, together with Esaïe Bauer, of the [[https://www.irif.fr/seminaires/picube/index|Formath seminar]], which is the seminar of Picube INRIA team. I am also responsible, with Pierre Clairambault and Chantal Keller, of [[https://www.irif.fr/gt-scalp/index|chairing the Scalp working group]] of GDR-IM and organizing its annual meetings. I am the PI of the ANR funded collaborative project [[https://www.irif.fr/reciprog/index|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.



==== Research interests ====
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

==== News ====

  * oct 23: I am organizing [[https://www.irif.fr/users/saurin/FICS2024/index.html|FICS workshop in february 2024]];
  * sep 23: I am organizing the [[https://www.irif.fr/gt-scalp/journees-2023|2023 annual meeting of SCALP working group, on 27-29 november in Orléans]];
  * sep 23: In september 2023, I presented my recent paper [[https://link.springer.com/chapter/10.1007/978-3-031-43513-3_12|on cut-elimination for full non-wellfounded linear logic with fixed-points]] published in TABLEAU 23. A long version is [[https://hal.science/hal-04169137|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. [[https://www.paris-univ-humaine.com/|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: [[https://jnim2023.sciencesconf.org/|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 [[https://www.irif.fr/gt-scalp/journees-2022|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 ([[https://www.irif.fr/gt-scalp/journees-2022/motion-17-02-2023|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. [[https://hal.science/hal-03682126|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 [[https://www.irif.fr/_media/users/saurin/pts-171121.pdf|Virtous circles in proofs]]. You can even find a video on the [[https://www.proofsociety.org/proof-theory-seminar/slides.html|website of the PTVS]].


/* 
==== Some talks ====

  * I gave an invited talk at the special session on logic in computer science, at Logic colloquium june 2022
  * I gave an invited talk at Strip workshop, in Birmingham, may 2022
  * An invited talk at the Virtual Proof Theory seminar
*/
==== Publications and drafts ====

== Published works ==

You can find an updated [[https://dblp.org/pid/19/1889.html|list of my publications on DBLP]].

/*Recent publications: */
  * 2023:
    * <html><div></html>[[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]])  <html><span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="tableaux23"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/>

<div class="bs-wrap bs-wrap-collapse collapse" id="tableaux23"><div class="bs-wrap bs-wrap-well well well-sm">
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]. <br/>
The paper studies a fixed-point encoding of LL exponentials in order to deduce those cut-elimination results from that of μMALL∞.  <br/>
Cut-elimination for μLK∞ and μLJ∞ is obtained by developing appropriate linear decorations for those logics.</div></div></html>
    * <html><div></html>[[https://arxiv.org/abs/2310.09038|On the exponential logic of sequentialization]], Aurore Alcolei, Luc Pellissier & Alexis Saurin, MFPS 2023 <html><span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="mfps23"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/>

<div class="bs-wrap bs-wrap-collapse collapse" id="mfps23"><div class="bs-wrap bs-wrap-well well well-sm">
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.</div></div></html>
    * <html><div></html>[[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  <html><span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="csl23"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/>

<div class="bs-wrap bs-wrap-collapse collapse" id="csl23"><div class="bs-wrap bs-wrap-well well well-sm">
 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.</div></div></html>
  * 2022
    *  <html><div></html>[[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  <html><span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="fsttcs22"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/>

<div class="bs-wrap bs-wrap-collapse collapse" id="fsttcs22"><div class="bs-wrap bs-wrap-well well well-sm">
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. 
<br />
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.</div></div></html>
    *  <html><div></html>[[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  <html><span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="fscd22"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/>

<div class="bs-wrap bs-wrap-collapse collapse" id="fscd22"><div class="bs-wrap bs-wrap-well well well-sm">
 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.
<br />
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. </div></div></html>
    * <html><div></html>[[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]])  <html><span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="lics22"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/>

<div class="bs-wrap bs-wrap-collapse collapse" id="lics22"><div class="bs-wrap bs-wrap-well well well-sm">
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.
<br />
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.
<br />
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.
</div></div></html>
  * 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: 
  * <html><div></html>[[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, to appear in FSTTCS 2023   <html><span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="fsttcs23"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/>
<div class="bs-wrap bs-wrap-collapse collapse" id="fsttcs23"><div class="bs-wrap bs-wrap-well well well-sm">
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.
<br />
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.
<br />
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.
</div></div></html>
  *  <html><div></html>[[https://www.irif.fr/_media/users/saurin/pub/nwf-circ-denot.pdf|On denotations of circular and non-wellfounded proofs]], with Thomas Ehrhard &Farzad Jafarrahmani, draft 2023  <html><span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="circ-denot23"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/>

<div class="bs-wrap bs-wrap-collapse collapse" id="circ-denot23"><div class="bs-wrap bs-wrap-well well well-sm">
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.
<br />
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.
</div></div></html>
  * <html><div></html>[[https://hal.science/hal-03655737v1|Polarized linear logic with fixpoints]], with Thomas Ehrhard & Farzad Jafarrahmani, draft 2022  <html><span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="polarized22"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/>

<div class="bs-wrap bs-wrap-collapse collapse" id="polarized22"><div class="bs-wrap bs-wrap-well well well-sm">
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. </div></div></html>


==== Teaching ====

This semester, I am 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-2023|Course on functional programming and formal proofs in Coq (PF2)]]

Last year, I was teachnig with Thomas Colcombet the course on 

  * [[https://www.irif.fr/users/saurin/teaching/lmfi/sofix-2023|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]]

== 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
  * 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 Students: ==
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 

==== Contact informations  ====


{{page>inc&noheader&nofooter}}