22 Search Results for "Kirst, Dominik"

Document
DOI: 10.4230/LIPIcs.CSL.2026.18
A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light

Authors: Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi

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

Abstract
We extend the existing HOL Light Library for Modal Systems (HOLMS) to support a modular implementation of modal reasoning within the HOL Light proof assistant. We deeply embed axiomatic calculi and relational semantics for seven normal modal logics (K, T, B, K4, S4, S5, GL) and formalise modal adequacy theorems for these systems. We then leverage those formalisations to implement a mechanism for automated reasoning via proof-search in the associated labelled sequent calculi, which we shallowly embed in HOL Light’s goal-stack mechanism. This way, we equip the general-purpose proof assistant with (semi)decision procedures for these logics that, in case of failure to construct a proof for the input formula, return a certified countermodel within the appropriate class for the logic under consideration. On the methodological side, we propose a precise measure of the modularity of our approach by systematically adopting Christopher Strachey’s distinction between ad hoc and parametric polymorphism throughout the library.
Cite as

Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi. A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 18:1-18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bilotta_et_al:LIPIcs.CSL.2026.18,
  author =	{Bilotta, Antonella and Maggesi, Marco and Perini Brogi, Cosimo},
  title =	{{A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{18:1--18:29},
  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.18},
  URN =		{urn:nbn:de:0030-drops-254427},
  doi =		{10.4230/LIPIcs.CSL.2026.18},
  annote =	{Keywords: Modal logic, HOL Light, Labelled sequent calculi, Logical verification, Interactive theorem proving, Automated proof-search}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.24
Well-Founded Coalgebras Meet Kőnig’s Lemma

Authors: Henning Urbat and Thorsten Wißmann

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

Abstract
Kőnig’s lemma is a fundamental result about trees with countless applications in mathematics and computer science. In contrapositive form, it states that if a tree is finitely branching and well-founded (i.e. has no infinite paths), then it is finite. We present a coalgebraic version of Kőnig’s lemma featuring two dimensions of generalization: from finitely branching trees to coalgebras for a finitary endofunctor H, and from the base category of sets to a locally finitely presentable category ℂ, such as the category of posets, nominal sets, or convex sets. Our coalgebraic Kőnig’s lemma states that, under mild assumptions on ℂ and H, every well-founded coalgebra for H is the directed join of its well-founded subcoalgebras with finitely generated state space - in particular, the category of well-founded coalgebras is locally presentable. As applications, we derive versions of Kőnig’s lemma for graphs in a topos as well as for nominal and convex transition systems. Additionally, we show that the key construction underlying the proof gives rise to two simple constructions of the initial algebra (equivalently, the final recursive coalgebra) for the functor H: The initial algebra is both the colimit of all well-founded and of all recursive coalgebras with finitely presentable state space. Remarkably, this result holds even in settings where well-founded coalgebras form a proper subclass of recursive ones. The first construction of the initial algebra is entirely new, while for the second one our approach yields a short and transparent new correctness proof.
Cite as

Henning Urbat and Thorsten Wißmann. Well-Founded Coalgebras Meet Kőnig’s Lemma. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{urbat_et_al:LIPIcs.CSL.2026.24,
  author =	{Urbat, Henning and Wi{\ss}mann, Thorsten},
  title =	{{Well-Founded Coalgebras Meet K\H{o}nig’s Lemma}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{24:1--24:19},
  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.24},
  URN =		{urn:nbn:de:0030-drops-254485},
  doi =		{10.4230/LIPIcs.CSL.2026.24},
  annote =	{Keywords: K\H{o}nig’s Lemma, Well-Foundedness, Coalgebra}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.8
Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting

Authors: Asta Halkjær From and Anders Schlichtkrull

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Smullyan and Fitting have used abstract consistency properties to great effect in unifying meta-theoretical results in logic. In this paper, we generalize these developments with the help of Isabelle/HOL. We use locales to decompose abstract consistency into general parts, and provide the textbook variants as special cases. Users can assemble their own consistency property for a given logic. The compositionality alleviates the absence of dependent types in Isabelle/HOL. We use our development to mechanize completeness of calculi for three logics: (1) first-order logic where we only instantiate universal quantifiers with already occurring terms, (2) second-order logic over general models, and (3) a recently developed strong hybrid logic with propositional quantification.
Cite as

Asta Halkjær From and Anders Schlichtkrull. Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{from_et_al:LIPIcs.ITP.2025.8,
  author =	{From, Asta Halkj{\ae}r and Schlichtkrull, Anders},
  title =	{{Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness \`{a} la Fitting}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.8},
  URN =		{urn:nbn:de:0030-drops-246406},
  doi =		{10.4230/LIPIcs.ITP.2025.8},
  annote =	{Keywords: Logic, completeness, abstract consistency property, Isabelle/HOL, locales}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.10
An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems

Authors: Dohan Kim

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We present a formalized framework for semi-Thue and conditional semi-Thue systems for studying monoids and their word problem using the Isabelle/HOL proof assistant. We provide a formalized decision procedure for the word problem of monoids if they are finitely presented by complete semi-Thue systems. In particular, we present a new formalized method for checking confluence using (conditional) critical pairs for certain conditional semi-Thue systems. We propose and formalize an inference system for generating conditional equational theories and Thue congruences using conditional semi-Thue systems. Then we provide a new formalized decision procedure for the word problem of monoids which have finite complete (reductive) conditional presentations.
Cite as

Dohan Kim. An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kim:LIPIcs.ITP.2025.10,
  author =	{Kim, Dohan},
  title =	{{An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{10:1--10:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.10},
  URN =		{urn:nbn:de:0030-drops-246081},
  doi =		{10.4230/LIPIcs.ITP.2025.10},
  annote =	{Keywords: semi-Thue systems, conditional semi-Thue systems, conditional string rewriting, monoids, word problem}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2025.1
Computation First: Rebuilding Constructivism with Effects (Invited Talk)

Authors: Liron Cohen

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

Abstract
Constructive logic and type theory have traditionally been grounded in pure, effect-free model of computation. This paper argues that such a restriction is not a foundational necessity but a historical artifact, and it advocates for a broader perspective of effectful constructivism, where computational effects, such as state, non-determinism, and exceptions, are directly and internally embedded in the logical and computational foundations. We begin by surveying examples where effects reshape logical principles, and then outline three approaches to effectful constructivism, focusing on realizability models: Monadic Combinatory Algebras, which extend classical partial combinatory algebras with effectful computation; Evidenced Frames, a flexible semantic structure capable of uniformly capturing a wide range of effects; and Effectful Higher-Order Logic (EffHOL), a syntactic approach that directly translates logical propositions into specifications for effectful programs. We further illustrate how concrete type theories can internalize effects, via the family of type theories TT^□_C. Together, these works demonstrate that effectful constructivism is not merely possible but a natural and robust extension of traditional frameworks.
Cite as

Liron Cohen. Computation First: Rebuilding Constructivism with Effects (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cohen:LIPIcs.FSCD.2025.1,
  author =	{Cohen, Liron},
  title =	{{Computation First: Rebuilding Constructivism with Effects}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{1:1--1:20},
  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.1},
  URN =		{urn:nbn:de:0030-drops-236167},
  doi =		{10.4230/LIPIcs.FSCD.2025.1},
  annote =	{Keywords: Effectful constructivism, realizability, type theory, monadic combinatory algebras, evidenced frame}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.33
Solving Guarded Domain Equations in Presheaves over Ordinals and Mechanizing It

Authors: Sergei Stepanenko and Amin Timany

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

Abstract
Constructing solutions to recursive domain equations is a well-known, important problem in the study of programs and programming languages. Mathematically speaking, the problem is finding a fixed point (up to isomorphism) of a suitable functor over a suitable category. A particularly useful instance, inspired by the step-indexing technique, is where the functor is over (a subcategory of) the category of presheaves over the ordinal ω and the functors are locally-contractive, also known as guarded functors. This corresponds to step-indexing over natural numbers. However, for certain problems, e.g., when dealing with infinite non-determinism, one needs to employ trans-finite step-indexing, i.e., consider presheaf categories over higher ordinals. Prior work on trans-finite step-indexing either only considers a very narrow class of functors over a particularly restricted subcategory of presheaves over higher ordinals, or treats the problem very generally working with sheaves over an arbitrary complete Heyting algebra with a well-founded basis. In this paper we present a solution to the guarded domain equations problem over all guarded functors over the category of presheaves over ordinal numbers, as well as its mechanization in the Rocq Prover. As the categories of sheaves and presheaves over ordinals are equivalent, our main contribution is simplifying prior work from the setting of the category of sheaves to the setting of the category of presheaves and mechanizing it - presheaves are more amenable to mechanization in a proof assistant.
Cite as

Sergei Stepanenko and Amin Timany. Solving Guarded Domain Equations in Presheaves over Ordinals and Mechanizing It. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 33:1-33:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{stepanenko_et_al:LIPIcs.FSCD.2025.33,
  author =	{Stepanenko, Sergei and Timany, Amin},
  title =	{{Solving Guarded Domain Equations in Presheaves over Ordinals and Mechanizing It}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{33:1--33:24},
  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.33},
  URN =		{urn:nbn:de:0030-drops-236486},
  doi =		{10.4230/LIPIcs.FSCD.2025.33},
  annote =	{Keywords: Domain Equations, Guarded Fixed Points, Fixed Points, Category Theory, Rocq, Presheaves, Ordinals}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.17
Mechanized Undecidability of Higher-Order Beta-Matching

Authors: Andrej Dudenhefner

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

Abstract
Higher-order β-matching is the following decision problem: given two simply typed λ-terms, can the first term be instantiated to be β-equivalent to the second term? This problem was formulated by Huet in the 1970s and shown undecidable by Loader in 2003 by reduction from λ-definability. The present work provides a novel undecidability proof for higher-order β-matching, in an effort to verify this result by means of a proof assistant. Rather than starting from λ-definability, the presented proof encodes a restricted form of string rewriting as higher-order β-matching. The particular approach is similar to Urzyczyn’s undecidability result for intersection type inhabitation. The presented approach has several advantages. First, the proof is simpler to verify in full detail due to the simple form of rewriting systems, which serve as a starting point. Second, undecidability of the considered problem in string rewriting is already certified using the Coq proof assistant. As a consequence, we obtain a certified many-one reduction from the Halting Problem to higher-order β-matching. Third, the presented approach identifies a uniform construction which shows undecidability of higher-order β-matching, λ-definability, and intersection type inhabitation. The presented undecidability proof is mechanized in the Coq proof assistant and contributed to the existing Coq Library of Undecidability Proofs.
Cite as

Andrej Dudenhefner. Mechanized Undecidability of Higher-Order Beta-Matching. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dudenhefner:LIPIcs.FSCD.2025.17,
  author =	{Dudenhefner, Andrej},
  title =	{{Mechanized Undecidability of Higher-Order Beta-Matching}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{17:1--17:15},
  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.17},
  URN =		{urn:nbn:de:0030-drops-236323},
  doi =		{10.4230/LIPIcs.FSCD.2025.17},
  annote =	{Keywords: lambda-calculus, simple types, undecidability, higher-order matching, mechanization, Coq}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.9
A Zoo of Continuity Properties in Constructive Type Theory

Authors: Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot, and Matthieu Piquerez

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

Abstract
Continuity principles stating that all functions are continuous play a central role in some schools of constructive mathematics. However, there are different ways to formalise the property of being continuous in constructive foundations. We analyse these continuity properties from the perspective of constructive reverse mathematics. We work in constructive type theory, which can be seen as a minimal foundation for constructive reverse mathematics. We treat continuity of functions F : (Q → A) → R, i.e. with question type Q, answer type A, and result type R. Concretely, we discuss continuity defined via moduli, making the relevant list L : LQ of questions explicit, dialogue trees, making the question-answer process explicit as inductive tree, and tree functions, making the question-answer process explicit as function. We prove equivalences where possible and isolate necessary and sufficient axioms for equivalence proofs. Many of the results we discuss are already present in the works of Hancock, Pattinson, Ghani, Kawai, Fujiwara, Brede, Herbelin, Escardó, and others. Our main contribution is their formulation over a uniform foundation, the observation that no choice axioms are necessary, the generalisation to arbitrary types from natural numbers where possible, and a mechanisation in the Coq/Rocq proof assistant.
Cite as

Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot, and Matthieu Piquerez. A Zoo of Continuity Properties in Constructive Type Theory. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{baillon_et_al:LIPIcs.FSCD.2025.9,
  author =	{Baillon, Martin and Forster, Yannick and Mahboubi, Assia and P\'{e}drot, Pierre-Marie and Piquerez, Matthieu},
  title =	{{A Zoo of Continuity Properties in Constructive Type Theory}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{9:1--9:20},
  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.9},
  URN =		{urn:nbn:de:0030-drops-236245},
  doi =		{10.4230/LIPIcs.FSCD.2025.9},
  annote =	{Keywords: type theory, constructive mathematics, continuity, Coq}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.14
From Partial to Monadic: Combinatory Algebra with Effects

Authors: Liron Cohen, Ariel Grunfeld, Dominik Kirst, and Étienne Miquey

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

Abstract
Partial Combinatory Algebras (PCAs) provide a foundational model of the untyped λ-calculus and serve as the basis for many notions of computability, such as realizability theory. However, PCAs support a very limited notion of computation by only incorporating non-termination as a computational effect. To provide a framework that better internalizes a wide range of computational effects, this paper puts forward the notion of Monadic Combinatory Algebras (MCAs). MCAs generalize the notion of PCAs by structuring the combinatory algebra over an underlying computational effect, embodied by a monad. We show that MCAs can support various side effects through the underlying monad, such as non-determinism, stateful computation and continuations. We further obtain a categorical characterization of MCAs within Freyd Categories, following a similar connection for PCAs. Moreover, we explore the application of MCAs in realizability theory, presenting constructions of effectful realizability triposes and assemblies derived through evidenced frames, thereby generalizing traditional PCA-based realizability semantics. The monadic generalization of the foundational notion of PCAs provides a comprehensive and powerful framework for internally reasoning about effectful computations, paving the path to a more encompassing study of computation and its relationship with realizability models and programming languages.
Cite as

Liron Cohen, Ariel Grunfeld, Dominik Kirst, and Étienne Miquey. From Partial to Monadic: Combinatory Algebra with Effects. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cohen_et_al:LIPIcs.FSCD.2025.14,
  author =	{Cohen, Liron and Grunfeld, Ariel and Kirst, Dominik and Miquey, \'{E}tienne},
  title =	{{From Partial to Monadic: Combinatory Algebra with Effects}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{14:1--14:22},
  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.14},
  URN =		{urn:nbn:de:0030-drops-236297},
  doi =		{10.4230/LIPIcs.FSCD.2025.14},
  annote =	{Keywords: Combinatory algebras, Monads, Effects, Realizability, Evidenced frames}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2025.3
Synthetic Mathematics for the Mechanisation of Computability Theory and Logic (Invited Talk)

Authors: Yannick Forster

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Mathematical practice in most areas of mathematics is based on the assumption that proofs could be made fully formal in a chosen foundation in principle. This assumption is backed by partial attempts at formalisation and by full mechanisation of various areas of mathematics in various proof assistants and various foundations. Areas that have been largely neglected for computer-assisted and machine-checked proofs are computability theory and logic: Fundamental results like Gödel’s second incompleteness theorem in its stronger forms due to Kleene and Rosser, Löb’s theorem, Post’s theorem connecting the arithmetical hierarchy and Turing jumps, or the Friedberg-Muĉnik theorem solving Post’s problem have not or only very recently been re-produced in proof assistants. This is due to the fact that making these arguments formal is several orders of magnitude more involved than formalising other areas of mathematics, due to the amount of invisible mathematics (a term coined by Andrej Bauer) involved. In computability theory, invisible arguments occur mainly behind proofs that a certain intuitively sketched procedure is computable in - citing Emil Post - "forbidding, diverse and alien formalisms in which this [...] work of Gödel, Church, Turing, Kleene, Rosser [...] is embodied.". For instance, there have been various approaches of formalising Turing machines, all to the ultimate dissatisfaction of the respective authors, and none going further than constructing a universal machine and proving the halting problem undecidable. Professional computability theorist and teachers of computability theory thus rely on the informal Church Turing thesis to carry out their work and only argue the computability of described algorithms informally. For computability theory, a way out was proposed in the 1980s by Fred Richman and developed during the last decade by Andrej Bauer: Synthetic computability theory, where one assumes axioms in a constructive foundation which essentially identify all (constructively definable) functions with computable functions. A drawback of the approach is that assuming such an axiom on top of the axiom of countable choice - which is routinely assumed in this branch of constructive mathematics and computable analysis - is that the law of excluded middle, i.e. classical logic, becomes invalid. Computability theory is however, as all mainstream branches of mathematics, making routine use of the axiom of excluded middle. In the case of logic, the invisible mathematics usually is either centered around encoding formulas and proofs as numbers using Gödel or similar encodings or about provability arguments that certain results can be proved in restricted proof systems such as Peano arithmetic. In several settings, synthetic computability arguments can be employed to mechanise these proofs. We observe that a slight foundational shift rectifies the situation: By basing synthetic computability theory in the Calculus of Inductive Constructions, the type theory underlying amongst others the Coq and Lean proof assistants, where countable choice is independent and thus not provable, axioms for synthetic computability are compatible with the law of excluded middle. This insight can be used to finally mechanise computability theory and logic, in an elegant, concise way where invisible arguments stay invisible: with Felix Jahn I have mechanised arguments related to many-one and truth-table reduction theory (published at CSL '23), Dominik Kirst and Benjamin Peters have presented Gödel’s first incompleteness theorem in this style (at CSL '23), and in collaboration with Dominik Kirst and Niklas Mück I have given a proof of Post’s hierarchy theorem (at CSL '24). In this invited talk, I will give a broader overview of this line of research investigating a mechanised synthetic approach to logic and computability theory. In particular, I will discuss a Coq library of undecidability proofs, results in the theory of reducibility degrees, constructive reverse analysis of theorems, as well as generalised incompleteness results such as Löb’s theorem.
Cite as

Yannick Forster. Synthetic Mathematics for the Mechanisation of Computability Theory and Logic (Invited Talk). In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{forster:LIPIcs.CSL.2025.3,
  author =	{Forster, Yannick},
  title =	{{Synthetic Mathematics for the Mechanisation of Computability Theory and Logic}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{3:1--3:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.3},
  URN =		{urn:nbn:de:0030-drops-227603},
  doi =		{10.4230/LIPIcs.CSL.2025.3},
  annote =	{Keywords: Synthetic mathematics, computability theory, logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.40
Completeness of First-Order Bi-Intuitionistic Logic

Authors: Dominik Kirst and Ian Shillito

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We provide a succinct and verified completeness proof for first-order bi-intuitionistic logic, relative to constant domain Kripke semantics. By doing so, we make up for the almost-50-year-old substantial mistakes in Rauszer’s foundational work, detected but unresolved by Shillito two years ago. Moreover, an even earlier but historically neglected proof by Klemke has been found to contain at least local errors by Olkhovikov and Badia, that remained unfixed due to the technical complexity of Klemke’s argument. To resolve this unclear situation once and for all, we give a succinct completeness proof, based on and dualising a standard proof for constant domain intuitionistic logic, and verify our constructions using the Coq proof assistant to guarantee correctness.
Cite as

Dominik Kirst and Ian Shillito. Completeness of First-Order Bi-Intuitionistic Logic. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 40:1-40:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kirst_et_al:LIPIcs.CSL.2025.40,
  author =	{Kirst, Dominik and Shillito, Ian},
  title =	{{Completeness of First-Order Bi-Intuitionistic Logic}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{40:1--40:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.40},
  URN =		{urn:nbn:de:0030-drops-227979},
  doi =		{10.4230/LIPIcs.CSL.2025.40},
  annote =	{Keywords: bi-intuitionistic logic, first-order logic, completeness, Coq proof assistant}
}
Document
DOI: 10.4230/LIPIcs.CSL.2024.29
The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions

Authors: Yannick Forster, Dominik Kirst, and Niklas Mück

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
The Kleene-Post theorem and Post’s theorem are two central and historically important results in the development of oracle computability theory, clarifying the structure of Turing reducibility degrees. They state, respectively, that there are incomparable Turing degrees and that the arithmetical hierarchy is connected to the relativised form of the halting problem defined via Turing jumps. We study these two results in the calculus of inductive constructions (CIC), the constructive type theory underlying the Coq proof assistant. CIC constitutes an ideal foundation for the formalisation of computability theory for two reasons: First, like in other constructive foundations, computable functions can be treated via axioms as a purely synthetic notion rather than being defined in terms of a concrete analytic model of computation such as Turing machines. Furthermore and uniquely, CIC allows consistently assuming classical logic via the law of excluded middle or weaker variants on top of axioms for synthetic computability, enabling both fully classical developments and taking the perspective of constructive reverse mathematics on computability theory. In the present paper, we give a fully constructive construction of two Turing-incomparable degrees à la Kleene-Post and observe that the classical content of Post’s theorem seems to be related to the arithmetical hierarchy of the law of excluded middle due to Akama et. al. Technically, we base our investigation on a previously studied notion of synthetic oracle computability and contribute the first consistency proof of a suitable enumeration axiom. All results discussed in the paper are mechanised and contributed to the Coq library of synthetic computability.
Cite as

Yannick Forster, Dominik Kirst, and Niklas Mück. The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.CSL.2024.29,
  author =	{Forster, Yannick and Kirst, Dominik and M\"{u}ck, Niklas},
  title =	{{The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.29},
  URN =		{urn:nbn:de:0030-drops-196728},
  doi =		{10.4230/LIPIcs.CSL.2024.29},
  annote =	{Keywords: Constructive mathematics, Computability theory, Logical foundations, Constructive type theory, Interactive theorem proving, Coq proof assistant}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.21
Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq

Authors: Yannick Forster and Felix Jahn

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
We present a constructive analysis and machine-checked theory of one-one, many-one, and truth-table reductions based on synthetic computability theory in the Calculus of Inductive Constructions, the type theory underlying the proof assistant Coq. We give elegant, synthetic, and machine-checked proofs of Post’s landmark results that a simple predicate exists, is enumerable, undecidable, but many-one incomplete (Post’s problem for many-one reducibility), and a hypersimple predicate exists, is enumerable, undecidable, but truth-table incomplete (Post’s problem for truth-table reducibility). In synthetic computability, one assumes axioms allowing to carry out computability theory with all definitions and proofs purely in terms of functions of the type theory with no mention of a model of computation. Proofs can focus on the essence of the argument, without having to sacrifice formality. Synthetic computability also clears the lense for constructivisation. Our constructively careful definition of simple and hypersimple predicates allows us to not assume classical axioms, not even Markov’s principle, still yielding the expected strong results.
Cite as

Yannick Forster and Felix Jahn. Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.CSL.2023.21,
  author =	{Forster, Yannick and Jahn, Felix},
  title =	{{Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{21:1--21:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.21},
  URN =		{urn:nbn:de:0030-drops-174820},
  doi =		{10.4230/LIPIcs.CSL.2023.21},
  annote =	{Keywords: type theory, computability theory, constructive mathematics, Coq}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.30
Gödel’s Theorem Without Tears - Essential Incompleteness in Synthetic Computability

Authors: Dominik Kirst and Benjamin Peters

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
Gödel published his groundbreaking first incompleteness theorem in 1931, stating that a large class of formal logics admits independent sentences which are neither provable nor refutable. This result, in conjunction with his second incompleteness theorem, established the impossibility of concluding Hilbert’s program, which pursued a possible path towards a single formal system unifying all of mathematics. Using a technical trick to refine Gödel’s original proof, the incompleteness result was strengthened further by Rosser in 1936 regarding the conditions imposed on the formal systems. Computability theory, which also originated in the 1930s, was quickly applied to formal logics by Turing, Kleene, and others to yield incompleteness results similar in strength to Gödel’s original theorem, but weaker than Rosser’s refinement. Only much later, Kleene found an improved but far less well-known proof based on computational notions, yielding a result as strong as Rosser’s. In this expository paper, we work in constructive type theory to reformulate Kleene’s incompleteness results abstractly in the setting of synthetic computability theory and assuming a form of Church’s thesis, an axiom internalising the fact that all functions definable in such a setting are computable. Our novel, greatly condensed reformulation showcases the simplicity of the computational argument while staying formally entirely precise, a combination hard to achieve in typical textbook presentations. As an application, we instantiate the abstract result to first-order logic in order to derive essential incompleteness and, along the way, essential undecidability of Robinson arithmetic. This paper is accompanied by a Coq mechanisation covering all our results and based on existing libraries of undecidability proofs and first-order logic, complementing the extensive work on mechanised incompleteness using the Gödel-Rosser approach. In contrast to the related mechanisations, our development follows Kleene’s ideas and utilises Church’s thesis for additional simplicity.
Cite as

Dominik Kirst and Benjamin Peters. Gödel’s Theorem Without Tears - Essential Incompleteness in Synthetic Computability. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kirst_et_al:LIPIcs.CSL.2023.30,
  author =	{Kirst, Dominik and Peters, Benjamin},
  title =	{{G\"{o}del’s Theorem Without Tears - Essential Incompleteness in Synthetic Computability}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{30:1--30:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.30},
  URN =		{urn:nbn:de:0030-drops-174911},
  doi =		{10.4230/LIPIcs.CSL.2023.30},
  annote =	{Keywords: incompleteness, undecidability, synthetic computability theory}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.12
Synthetic Kolmogorov Complexity in Coq

Authors: Yannick Forster, Fabian Kunze, and Nils Lauermann

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
We present a generalised, constructive, and machine-checked approach to Kolmogorov complexity in the constructive type theory underlying the Coq proof assistant. By proving that nonrandom numbers form a simple predicate, we obtain elegant proofs of undecidability for random and nonrandom numbers and a proof of uncomputability of Kolmogorov complexity. We use a general and abstract definition of Kolmogorov complexity and subsequently instantiate it to several definitions frequently found in the literature. Whereas textbook treatments of Kolmogorov complexity usually rely heavily on classical logic and the axiom of choice, we put emphasis on the constructiveness of all our arguments, however without blurring their essence. We first give a high-level proof idea using classical logic, which can be formalised with Markov’s principle via folklore techniques we subsequently explain. Lastly, we show a strategy how to eliminate Markov’s principle from a certain class of computability proofs, rendering all our results fully constructive. All our results are machine-checked by the Coq proof assistant, which is enabled by using a synthetic approach to computability: rather than formalising a model of computation, which is well known to introduce a considerable overhead, we abstractly assume a universal function, allowing the proofs to focus on the mathematical essence.
Cite as

Yannick Forster, Fabian Kunze, and Nils Lauermann. Synthetic Kolmogorov Complexity in Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.ITP.2022.12,
  author =	{Forster, Yannick and Kunze, Fabian and Lauermann, Nils},
  title =	{{Synthetic Kolmogorov Complexity in Coq}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{12:1--12:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.12},
  URN =		{urn:nbn:de:0030-drops-167219},
  doi =		{10.4230/LIPIcs.ITP.2022.12},
  annote =	{Keywords: Kolmogorov complexity, computability theory, random numbers, constructive matemathics, synthetic computability theory, constructive type theory, Coq}
}
  • Refine by Type
  • 22 Document/PDF
  • 9 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 9 2025
  • 1 2024
  • 2 2023
  • 4 2022
  • Show More...

  • Refine by Author
  • 8 Forster, Yannick
  • 8 Kirst, Dominik
  • 2 Cohen, Liron
  • 2 Dudenhefner, Andrej
  • 2 Hermes, Marc
  • Show More...

  • Refine by Series/Journal
  • 22 LIPIcs

  • Refine by Classification
  • 12 Theory of computation → Type theory
  • 11 Theory of computation → Constructive mathematics
  • 7 Theory of computation → Logic and verification
  • 3 Theory of computation → Modal and temporal logics
  • 3 Theory of computation → Proof theory
  • Show More...

  • Refine by Keyword
  • 11 Coq
  • 5 computability theory
  • 5 undecidability
  • 4 constructive type theory
  • 4 first-order 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