2 Search Results for "Nollet, Rémi"

Document
DOI: 10.4230/LIPIcs.FSTTCS.2022.35
Phase Semantics for Linear Logic with Least and Greatest Fixed Points

Authors: Abhishek De, Farzad Jafarrahmani, and Alexis Saurin

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)

Abstract
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.
Cite as

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-dev.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
DOI: 10.4230/LIPIcs.CSL.2018.35
Local Validity for Circular Proofs in Linear Logic with Fixed Points

Authors: Rémi Nollet, Alexis Saurin, and Christine Tasson

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

Abstract
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.
Cite as

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-dev.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}
}
  • Refine by Author
  • 2 Saurin, Alexis
  • 1 De, Abhishek
  • 1 Jafarrahmani, Farzad
  • 1 Nollet, Rémi
  • 1 Tasson, Christine

  • Refine by Classification
  • 2 Theory of computation → Linear logic
  • 2 Theory of computation → Proof theory
  • 1 Theory of computation → Logic
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 2 fixed points
  • 1 Linear logic
  • 1 circular proofs
  • 1 closure ordinals
  • 1 coinduction
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2018
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact