2 Search Results for "Pinault, Laureline"

Document
DOI: 10.4230/LIPIcs.FSCD.2021.29
On the Logical Strength of Confluence and Normalisation for Cyclic Proofs

Authors: Anupam Das

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
In this work we address the logical strength of confluence and normalisation for non-wellfounded typing derivations, in the tradition of "cyclic proof theory". We present a circular version CT of Gödel's system T, with the aim of comparing the relative expressivity of the theories CT and T. We approach this problem by formalising rewriting-theoretic results such as confluence and normalisation for the underlying "coterm" rewriting system of CT within fragments of second-order arithmetic. We establish confluence of CT within the theory RCA₀, a conservative extension of primitive recursive arithmetic and IΣ1. This allows us to recast type structures of hereditarily recursive operations as "coterm" models of T. We show that these also form models of CT, by formalising a totality argument for circular typing derivations within suitable fragments of second-order arithmetic. Relying on well-known proof mining results, we thus obtain an interpretation of CT into T; in fact, more precisely, we interpret level-n-CT into level-(n+1)-T, an optimum result in terms of abstraction complexity. A direct consequence of these model-theoretic results is weak normalisation for CT. As further results, we also show strong normalisation for CT and continuity of functionals computed by its type 2 coterms.
Cite as

Anupam Das. On the Logical Strength of Confluence and Normalisation for Cyclic Proofs. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 29:1-29:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{das:LIPIcs.FSCD.2021.29,
  author =	{Das, Anupam},
  title =	{{On the Logical Strength of Confluence and Normalisation for Cyclic Proofs}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{29:1--29:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.29},
  URN =		{urn:nbn:de:0030-drops-142678},
  doi =		{10.4230/LIPIcs.FSCD.2021.29},
  annote =	{Keywords: confluence, normalisation, system T, circular proofs, reverse mathematics, type structures}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2019.45
Cyclic Proofs and Jumping Automata

Authors: Denis Kuperberg, Laureline Pinault, and Damien Pous

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
We consider a fragment of a cyclic sequent proof system for Kleene algebra, and we see it as a computational device for recognising languages of words. The starting proof system is linear and we show that it captures precisely the regular languages. When adding the standard contraction rule, the expressivity raises significantly; we characterise the corresponding class of languages using a new notion of multi-head finite automata, where heads can jump.
Cite as

Denis Kuperberg, Laureline Pinault, and Damien Pous. Cyclic Proofs and Jumping Automata. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 45:1-45:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kuperberg_et_al:LIPIcs.FSTTCS.2019.45,
  author =	{Kuperberg, Denis and Pinault, Laureline and Pous, Damien},
  title =	{{Cyclic Proofs and Jumping Automata}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{45:1--45:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.45},
  URN =		{urn:nbn:de:0030-drops-116071},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.45},
  annote =	{Keywords: Cyclic proofs, regular languages, multi-head automata, transducers}
}
  • Refine by Author
  • 1 Das, Anupam
  • 1 Kuperberg, Denis
  • 1 Pinault, Laureline
  • 1 Pous, Damien

  • Refine by Classification
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Higher order logic
  • 1 Theory of computation → Lambda calculus
  • 1 Theory of computation → Logic
  • 1 Theory of computation → Proof theory

  • Refine by Keyword
  • 1 Cyclic proofs
  • 1 circular proofs
  • 1 confluence
  • 1 multi-head automata
  • 1 normalisation
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2019
  • 1 2021

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