Document

**Published in:** LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Extensions of Girard’s linear logic by least and greatest fixed point operators (μMALL) 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 (μMALL^∞) vs. infinitely branching well-founded proofs (μMALL_{ω,∞}). Our main result is that μMALL^∞ is strictly contained in μMALL_{ω,∞}.
For inclusion, we devise a novel technique involving infinitary rewriting of non-wellfounded proofs that yields a wellfounded proof in the limit. For strictness of the inclusion, we improve previously known lower bounds on μMALL^∞ provability from Π⁰₁-hard to Σ¹₁-hard, by encoding a sort of Büchi condition for Minsky machines.

Anupam Das, Abhishek De, and Alexis Saurin. Comparing Infinitary Systems for Linear Logic with Fixed Points. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 40:1-40:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{das_et_al:LIPIcs.FSTTCS.2023.40, author = {Das, Anupam and De, Abhishek and Saurin, Alexis}, title = {{Comparing Infinitary Systems for Linear Logic with Fixed Points}}, booktitle = {43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)}, pages = {40:1--40:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-304-1}, ISSN = {1868-8969}, year = {2023}, volume = {284}, editor = {Bouyer, Patricia and Srinivasan, Srikanth}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.40}, URN = {urn:nbn:de:0030-drops-194131}, doi = {10.4230/LIPIcs.FSTTCS.2023.40}, annote = {Keywords: linear logic, fixed points, non-wellfounded proofs, omega-branching proofs, analytical hierarchy} }

Document

**Published in:** LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (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.

Kostia Chardonnet, Alexis Saurin, and Benoît Valiron. A Curry-Howard Correspondence for Linear, Reversible Computation. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chardonnet_et_al:LIPIcs.CSL.2023.13, author = {Chardonnet, Kostia and Saurin, Alexis and Valiron, Beno\^{i}t}, title = {{A Curry-Howard Correspondence for Linear, Reversible Computation}}, booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)}, pages = {13:1--13:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-264-8}, ISSN = {1868-8969}, year = {2023}, volume = {252}, editor = {Klin, Bartek and Pimentel, Elaine}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.13}, URN = {urn:nbn:de:0030-drops-174747}, doi = {10.4230/LIPIcs.CSL.2023.13}, annote = {Keywords: Reversible Computation, Linear Logic, Curry-Howard} }

Document

**Published in:** LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (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.

Abhishek De, Farzad Jafarrahmani, and Alexis Saurin. Phase Semantics for Linear Logic with Least and Greatest Fixed Points. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 35:1-35:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{de_et_al:LIPIcs.FSTTCS.2022.35, author = {De, Abhishek and Jafarrahmani, Farzad and Saurin, Alexis}, title = {{Phase Semantics for Linear Logic with Least and Greatest Fixed Points}}, booktitle = {42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)}, pages = {35:1--35:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-261-7}, ISSN = {1868-8969}, year = {2022}, volume = {250}, editor = {Dawar, Anuj and Guruswami, Venkatesan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.35}, URN = {urn:nbn:de:0030-drops-174272}, doi = {10.4230/LIPIcs.FSTTCS.2022.35}, annote = {Keywords: Linear logic, fixed points, phase semantics, closure ordinals, cut elimination} }

Document

**Published in:** LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (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.

Anupam Das, Abhishek De, and Alexis Saurin. Decision Problems for Linear Logic with Least and Greatest Fixed Points. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{das_et_al:LIPIcs.FSCD.2022.20, author = {Das, Anupam and De, Abhishek and Saurin, Alexis}, title = {{Decision Problems for Linear Logic with Least and Greatest Fixed Points}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {20:1--20:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-233-4}, ISSN = {1868-8969}, year = {2022}, volume = {228}, editor = {Felty, Amy P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.20}, URN = {urn:nbn:de:0030-drops-163019}, doi = {10.4230/LIPIcs.FSCD.2022.20}, annote = {Keywords: Linear logic, fixed points, decidability, vector addition systems} }

Document

**Published in:** LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Circular (ie. non-wellfounded but regular) proofs have received increasing interest in recent years with the simultaneous development of their applications and meta-theory: infinitary proof theory is now well-established in several proof-theoretical frameworks such as Martin Löf's inductive predicates, linear logic with fixed points, etc. In the setting of non-wellfounded proofs, a validity criterion is necessary to distinguish, among all infinite derivation trees (aka. pre-proofs), those which are logically valid proofs. A standard approach is to consider a pre-proof to be valid if every infinite branch is supported by an infinitely progressing thread.
The paper focuses on circular proofs for MALL with fixed points. Among all representations of valid circular proofs, a new fragment is described, based on a stronger validity criterion. This new criterion is based on a labelling of formulas and proofs, whose validity is purely local. This allows this fragment to be easily handled, while being expressive enough to still contain all circular embeddings of Baelde's muMALL finite proofs with (co)inductive invariants: in particular deciding validity and computing a certifying labelling can be done efficiently. Moreover the Brotherston-Simpson conjecture holds for this fragment: every labelled representation of a circular proof in the fragment is translated into a standard finitary proof. Finally we explore how to extend these results to a bigger fragment, by relaxing the labelling discipline while retaining (i) the ability to locally certify the validity and (ii) to some extent, the ability to finitize circular proofs.

Rémi Nollet, Alexis Saurin, and Christine Tasson. Local Validity for Circular Proofs in Linear Logic with Fixed Points. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 35:1-35:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{nollet_et_al:LIPIcs.CSL.2018.35, author = {Nollet, R\'{e}mi and Saurin, Alexis and Tasson, Christine}, title = {{Local Validity for Circular Proofs in Linear Logic with Fixed Points}}, booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)}, pages = {35:1--35:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-088-0}, ISSN = {1868-8969}, year = {2018}, volume = {119}, editor = {Ghica, Dan R. and Jung, Achim}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.35}, URN = {urn:nbn:de:0030-drops-97025}, doi = {10.4230/LIPIcs.CSL.2018.35}, annote = {Keywords: sequent calculus, non-wellfounded proofs, circular proofs, induction, coinduction, fixed points, proof-search, linear logic, muMALL, finitization, infinite descent} }

Document

**Published in:** LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Infinitary and regular proofs are commonly used in fixed point logics. Being natural intermediate devices between semantics and traditional finitary proof systems, they are commonly found in completeness arguments, automated deduction, verification, etc. However, their proof theory is surprisingly underdeveloped. In particular, very little is known about the computational behavior of such proofs through cut elimination. Taking such aspects into account has unlocked rich developments at the intersection of proof theory and programming language theory. One would hope that extending this to infinitary calculi would lead, e.g., to a better understanding of recursion and corecursion in programming languages. Structural proof theory is notably based on two fundamental properties of a proof system: cut elimination and focalization. The first one is only known to hold for restricted (purely additive) infinitary calculi, thanks to the work of Santocanale and Fortier; the second one has never been studied in infinitary systems. In this paper, we consider the infinitary proof system muMALLi for multiplicative and additive linear logic extended with least and greatest fixed points, and prove these two key results. We thus establish muMALLi as a satisfying computational proof system in itself, rather than just an intermediate device in the study of finitary proof systems.

David Baelde, Amina Doumane, and Alexis Saurin. Infinitary Proof Theory: the Multiplicative Additive Case. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{baelde_et_al:LIPIcs.CSL.2016.42, author = {Baelde, David and Doumane, Amina and Saurin, Alexis}, title = {{Infinitary Proof Theory: the Multiplicative Additive Case}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {42:1--42:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.42}, URN = {urn:nbn:de:0030-drops-65825}, doi = {10.4230/LIPIcs.CSL.2016.42}, annote = {Keywords: Infinitary proofs, linear logic} }

Document

**Published in:** LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Various logics have been introduced in order to reason over (co)inductive specifications and, through the Curry-Howard correspondence, to study computation over inductive and coinductive data. The logic mu-MALL is one of those logics, extending multiplicative and additive linear logic with least and greatest fixed point operators.
In this paper, we investigate the semantics of mu-MALL proofs in (computational) ludics. This framework is built around the notion of design, which can be seen as an analogue of the strategies of game semantics. The infinitary nature of designs makes them particularly well suited for representing computations over infinite data.
We provide mu-MALL with a denotational semantics, interpreting proofs by designs and formulas by particular sets of designs called behaviours. Then we prove a completeness result for the class of "essentially finite designs", which are those designs performing a finite computation followed by a copycat. On the way to completeness, we investigate semantic inclusion, proving its decidability (given two formulas, we can decide whether the semantics of one is included in the other's) and completeness (if semantic inclusion holds, the corresponding implication is provable in mu-MALL).

David Baelde, Amina Doumane, and Alexis Saurin. Least and Greatest Fixed Points in Ludics. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 549-566, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{baelde_et_al:LIPIcs.CSL.2015.549, author = {Baelde, David and Doumane, Amina and Saurin, Alexis}, title = {{Least and Greatest Fixed Points in Ludics}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {549--566}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.549}, URN = {urn:nbn:de:0030-drops-54374}, doi = {10.4230/LIPIcs.CSL.2015.549}, annote = {Keywords: proof theory, fixed points, linear logic, ludics, game semantics, completeness, circular proofs, infinitary proof systems} }