3 Search Results for "Riba, Colin"

Document
DOI: 10.4230/LIPIcs.FSCD.2023.27
Cyclic Proofs for Arithmetical Inductive Definitions

Authors: Anupam Das and Lukas Melgaard

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
We investigate the cyclic proof theory of extensions of Peano Arithmetic by (finitely iterated) inductive definitions. Such theories are essential to proof theoretic analyses of certain "impredicative" theories; moreover, our cyclic systems naturally subsume Simpson’s Cyclic Arithmetic. Our main result is that cyclic and inductive systems for arithmetical inductive definitions are equally powerful. We conduct a metamathematical argument, formalising the soundness of cyclic proofs within second-order arithmetic by a form of induction on closure ordinals, thence appealing to conservativity results. This approach is inspired by those of Simpson and Das for Cyclic Arithmetic, however we must further address a difficulty: the closure ordinals of our inductive definitions (around Church-Kleene) far exceed the proof theoretic ordinal of the appropriate metatheory (around Bachmann-Howard), so explicit induction on their notations is not possible. For this reason, we rather rely on formalisation of the theory of (recursive) ordinals within second-order arithmetic.
Cite as

Anupam Das and Lukas Melgaard. Cyclic Proofs for Arithmetical Inductive Definitions. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{das_et_al:LIPIcs.FSCD.2023.27,
  author =	{Das, Anupam and Melgaard, Lukas},
  title =	{{Cyclic Proofs for Arithmetical Inductive Definitions}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{27:1--27:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.27},
  URN =		{urn:nbn:de:0030-drops-180119},
  doi =		{10.4230/LIPIcs.FSCD.2023.27},
  annote =	{Keywords: cyclic proofs, inductive definitions, arithmetic, fixed points, proof theory}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.30
A Curry-Howard Approach to Church's Synthesis

Authors: Pierre Pradic and Colin Riba

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
Church's synthesis problem asks whether there exists a finite-state stream transducer satisfying a given input-output specification. For specifications written in Monadic Second-Order Logic over infinite words, Church's synthesis can theoretically be solved algorithmically using automata and games. We revisit Church's synthesis via the Curry-Howard correspondence by introducing SMSO, a non-classical subsystem of MSO, which is shown to be sound and complete w.r.t. synthesis thanks to an automata-based realizability model.
Cite as

Pierre Pradic and Colin Riba. A Curry-Howard Approach to Church's Synthesis. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{pradic_et_al:LIPIcs.FSCD.2017.30,
  author =	{Pradic, Pierre and Riba, Colin},
  title =	{{A Curry-Howard Approach to Church's Synthesis}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.30},
  URN =		{urn:nbn:de:0030-drops-77198},
  doi =		{10.4230/LIPIcs.FSCD.2017.30},
  annote =	{Keywords: Intuitionistic Arithmetic, Realizability, Monadic Second-Order Logic on Infinite Words}
}
Document
DOI: 10.4230/LIPIcs.TLCA.2015.302
Fibrations of Tree Automata

Authors: Colin Riba

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract
We propose a notion of morphisms between tree automata based on game semantics. Morphisms are winning strategies on a synchronous restriction of the linear implication between acceptance games. This leads to split indexed categories, with substitution based on a suitable notion of synchronous tree function. By restricting to tree functions issued from maps on alphabets, this gives a fibration of tree automata. We then discuss the (fibrewise) monoidal structure issued from the synchronous product of automata. We also discuss how a variant of the usual projection operation on automata leads to an existential quantification in the fibered sense. Our notion of morphism is correct (it respects language inclusion), and in a weaker sense also complete.
Cite as

Colin Riba. Fibrations of Tree Automata. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 302-316, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{riba:LIPIcs.TLCA.2015.302,
  author =	{Riba, Colin},
  title =	{{Fibrations of Tree Automata}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{302--316},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.302},
  URN =		{urn:nbn:de:0030-drops-51719},
  doi =		{10.4230/LIPIcs.TLCA.2015.302},
  annote =	{Keywords: Tree automata, Game semantics, Categorical logic.}
}
  • Refine by Author
  • 2 Riba, Colin
  • 1 Das, Anupam
  • 1 Melgaard, Lukas
  • 1 Pradic, Pierre

  • Refine by Classification
  • 1 Theory of computation → Proof theory

  • Refine by Keyword
  • 1 Categorical logic.
  • 1 Game semantics
  • 1 Intuitionistic Arithmetic
  • 1 Monadic Second-Order Logic on Infinite Words
  • 1 Realizability
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2015
  • 1 2017
  • 1 2023

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