2 Search Results for "Fortier, J�r�me"

Document
DOI: 10.4230/LIPIcs.CSL.2016.42
Infinitary Proof Theory: the Multiplicative Additive Case

Authors: David Baelde, Amina Doumane, and Alexis Saurin

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

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

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-dev.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
DOI: 10.4230/LIPIcs.CSL.2013.248
Cuts for circular proofs: semantics and cut-elimination

Authors: Jérôme Fortier and Luigi Santocanale

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
One of the authors introduced in [Santocanale, FoSSaCS, 2002] a calculus of circular proofs for studying the computability arising from the following categorical operations: finite products, finite coproducts, initial algebras, final coalgebras. The calculus presented [Santocanale, FoSSaCS, 2002] is cut-free; even if sound and complete for provability, it lacked an important property for the semantics of proofs, namely fullness w.r.t. the class of intended categorical models (called mu-bicomplete categories in [Santocanale, ITA, 2002]). In this paper we fix this problem by adding the cut rule to the calculus and by modifying accordingly the syntactical constraint ensuring soundness of proofs. The enhanced proof system fully represents arrows of the canonical model (a free mu-bicomplete category). We also describe a cut-elimination procedure as a a model of computation arising from the above mentioned categorical operations. The procedure constructs a cut-free proof-tree with possibly infinite branches out of a finite circular proof with cuts.
Cite as

Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 248-262, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{fortier_et_al:LIPIcs.CSL.2013.248,
  author =	{Fortier, J\'{e}r\^{o}me and Santocanale, Luigi},
  title =	{{Cuts for circular proofs: semantics and cut-elimination}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{248--262},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.248},
  URN =		{urn:nbn:de:0030-drops-42019},
  doi =		{10.4230/LIPIcs.CSL.2013.248},
  annote =	{Keywords: categorical proof-theory, fixpoints, initial and final (co)algebras, inductive and coinductive types}
}
  • Refine by Author
  • 1 Baelde, David
  • 1 Doumane, Amina
  • 1 Fortier, Jérôme
  • 1 Santocanale, Luigi
  • 1 Saurin, Alexis

  • Refine by Classification

  • Refine by Keyword
  • 1 Infinitary proofs
  • 1 categorical proof-theory
  • 1 fixpoints
  • 1 inductive and coinductive types
  • 1 initial and final (co)algebras
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2013
  • 1 2016

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