4 Search Results for "Kahle, Reinhard"

Document
DOI: 10.4230/LIPIcs.CSL.2026.17
A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials

Authors: Alexis Saurin and Esaïe Bauer

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
In the realm of light logics deriving from linear logic, a number of variants of exponential rules have been investigated. The profusion of such proof systems induces the need for cut-elimination theorems for each logic, the proofs of which may be redundant. A number of approaches in proof theory have been adopted to cope with this need. In the present paper, we consider this issue from the point of view of enhancing linear logic with least and greatest fixed-points and considering such a variety of exponential connectives. Our main contribution is to provide a uniform cut-elimination theorem for a parametrized system with fixed-points by combining two approaches: cut-elimination proofs by reduction (or translation) to another system and the identification of sufficient conditions for cut-elimination. More precisely, we examine a broad range of systems, taking inspiration from Nigam and Miller’s subexponentials and from the first author and Laurent’s super exponentials. Our work is motivated, on the one hand, by Baillot’s work on light logics with recursive types and on the other hand by our recent work on the proof theory of the modal μ-calculus.
Cite as

Alexis Saurin and Esaïe Bauer. A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 17:1-17:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{saurin_et_al:LIPIcs.CSL.2026.17,
  author =	{Saurin, Alexis and Bauer, Esa\"{i}e},
  title =	{{A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{17:1--17:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.17},
  URN =		{urn:nbn:de:0030-drops-254418},
  doi =		{10.4230/LIPIcs.CSL.2026.17},
  annote =	{Keywords: cut elimination, exponential modalities, fixed-points, linear logic, light logics, mu-calculus, non-wellfounded proofs, proof theory, sequent calculus, subexponentials, super exponentials}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.32
Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation

Authors: Alexis Saurin

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Analyzing Maehara’s method for proving Craig’s interpolation theorem, we extract a "proof relevant" interpolation theorem for first-order LL in the sense that if π is a cut-free sequent proof of A⊢ B, we can find a formula C in the common vocabulary of A and B and proofs π₁,π₂ of A⊢ C and C⊢ B respectively such that π₁ composed with π₂ cut-reduces to π. As a direct corollary, we get similar proof relevant interpolation results for LJ and LK using linear translations. This refined interpolation is then rephrased in terms of a cut-introduction process synthetizing the interpolant. Finally, we analyze the computational content of interpolation by proving an interpolation result for Curien and Herbelin’s Duality of Computation.
Cite as

Alexis Saurin. Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 32:1-32:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{saurin:LIPIcs.FSCD.2025.32,
  author =	{Saurin, Alexis},
  title =	{{Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{32:1--32:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.32},
  URN =		{urn:nbn:de:0030-drops-236478},
  doi =		{10.4230/LIPIcs.FSCD.2025.32},
  annote =	{Keywords: Classical Logic, Interpolation, Cut Elimination, Linear Logic, Sequent calculus, System L}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.35
A Recursion-Theoretic Characterization of the Probabilistic Class PP

Authors: Ugo Dal Lago, Reinhard Kahle, and Isabel Oitavem

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
Probabilistic complexity classes, despite capturing the notion of feasibility, have escaped any treatment by the tools of so-called implicit-complexity. Their inherently semantic nature is of course a barrier to the characterization of classes like BPP or ZPP, but not all classes are semantic. In this paper, we introduce a recursion-theoretic characterization of the probabilistic class PP, using recursion schemata with pointers.
Cite as

Ugo Dal Lago, Reinhard Kahle, and Isabel Oitavem. A Recursion-Theoretic Characterization of the Probabilistic Class PP. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 35:1-35:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.MFCS.2021.35,
  author =	{Dal Lago, Ugo and Kahle, Reinhard and Oitavem, Isabel},
  title =	{{A Recursion-Theoretic Characterization of the Probabilistic Class PP}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{35:1--35:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.35},
  URN =		{urn:nbn:de:0030-drops-144754},
  doi =		{10.4230/LIPIcs.MFCS.2021.35},
  annote =	{Keywords: Implicit complexity, tree-recursion, probabilistic classes, polynomial time, PP}
}
Document
DOI: 10.4230/DagSemRep.322
Proof Theory in Computer Science (Dagstuhl Seminar 01411)

Authors: Reinhard Kahle, Peter Schröder-Heister, and Robert F. Stärk

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Reinhard Kahle, Peter Schröder-Heister, and Robert F. Stärk. Proof Theory in Computer Science (Dagstuhl Seminar 01411). Dagstuhl Seminar Report 322, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2002)

Copy BibTex To Clipboard

@TechReport{kahle_et_al:DagSemRep.322,
  author =	{Kahle, Reinhard and Schr\"{o}der-Heister, Peter and St\"{a}rk, Robert F.},
  title =	{{Proof Theory in Computer Science (Dagstuhl Seminar 01411)}},
  pages =	{1--18},
  ISSN =	{1619-0203},
  year =	{2002},
  type = 	{Dagstuhl Seminar Report},
  number =	{322},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.322},
  URN =		{urn:nbn:de:0030-drops-152062},
  doi =		{10.4230/DagSemRep.322},
}
  • Refine by Type
  • 4 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2025
  • 1 2021
  • 1 2002

  • Refine by Author
  • 2 Kahle, Reinhard
  • 2 Saurin, Alexis
  • 1 Bauer, Esaïe
  • 1 Dal Lago, Ugo
  • 1 Oitavem, Isabel
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs
  • 1 DagSemRep

  • Refine by Classification
  • 2 Theory of computation → Linear logic
  • 2 Theory of computation → Proof theory
  • 1 Theory of computation → Lambda calculus
  • 1 Theory of computation → Recursive functions

  • Refine by Keyword
  • 1 Classical Logic
  • 1 Cut Elimination
  • 1 Implicit complexity
  • 1 Interpolation
  • 1 Linear Logic
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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