Dominik Kirst

38 papers A* 3B 15C 1Misc 2Journal 15Unranked 2
YearRankTypeTitle / Venue / Authors
2026 J jnl
Blurred Drinker Paradoxes and Blurred Choice Axioms: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem.
CoRR
Dominik Kirst, Haoyi Zeng
2025 B conf
Completeness of First-Order Bi-Intuitionistic Logic.
CSL
Dominik Kirst, Ian Shillito
2025 B conf
From Partial to Monadic: Combinatory Algebra with Effects.
FSCD
Liron Cohen, Ariel Grunfeld, Dominik Kirst, Étienne Miquey
2025 J jnl
From Partial to Monadic: Combinatory Algebra with Effects.
CoRR
Liron Cohen, Ariel Grunfeld, Dominik Kirst, Étienne Miquey
2025 A* conf
Syntactic Effectful Realizability in Higher-Order Logic.
LICS
Liron Cohen, Ariel Grunfeld, Dominik Kirst, Étienne Miquey
2025 J jnl
Syntactic Effectful Realizability in Higher-Order Logic.
CoRR
Liron Cohen, Ariel Grunfeld, Dominik Kirst, Étienne Miquey
2025 A* conf
The Blurred Drinker Paradox: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem.
LICS
Dominik Kirst, Haoyi Zeng
2024 B conf
A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic.
CPP
Ian Shillito, Dominik Kirst
2024 J jnl
An Analysis of Tennenbaum's Theorem in Constructive Type Theory.
Log. Methods Comput. Sci.
Marc Hermes, Dominik Kirst
2024 J jnl
Material dialogues for first-order logic in constructive type theory: extended version.
Math. Struct. Comput. Sci.
Dominik Wehr, Dominik Kirst
2024 A* conf
Separating Markov's Principles.
LICS
Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, Vincent Rahli
2024 B conf
The Kleene-Post and Post's Theorem in the Calculus of Inductive Constructions.
CSL
Yannick Forster, Dominik Kirst, Niklas Mück
2023 J jnl
An Analysis of Tennenbaum's Theorem in Constructive Type Theory.
CoRR
Marc Hermes, Dominik Kirst
2023 B conf
Gödel's Theorem Without Tears - Essential Incompleteness in Synthetic Computability.
CSL
Dominik Kirst, Benjamin Peters
2023 B conf
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions.
APLAS
Yannick Forster, Dominik Kirst, Niklas Mück
2023 J jnl
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions.
CoRR
Yannick Forster, Dominik Kirst, Niklas Mück
2023 J jnl
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq.
J. Autom. Reason.
Dominik Kirst, Marc Hermes
2022 B conf
An Analysis of Tennenbaum's Theorem in Constructive Type Theory.
FSCD
Marc Hermes, Dominik Kirst
2022 B conf
Computational Back-And-Forth Arguments in Constructive Type Theory.
ITP
Dominik Kirst
2022 Misc conf
Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic.
LFCS
Christian Hagemeier, Dominik Kirst
2022 J jnl
Constructive and mechanised meta-theory of IEL and similar modal logics.
J. Log. Comput.
Christian Hagemeier, Dominik Kirst
2022 C conf
Material Dialogues for First-Order Logic in Constructive Type Theory.
WoLLIC
Dominik Wehr, Dominik Kirst
2022 J jnl
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens.
Log. Methods Comput. Sci.
Dominik Kirst, Dominique Larchey-Wendling
2022 B conf
Undecidability of Dyadic First-Order Logic in Coq.
ITP
Johannes Hostert, Andrej Dudenhefner, Dominik Kirst
2022 B conf
Undecidability, incompleteness, and completeness of second-order logic in Coq.
CPP
Mark Koch, Dominik Kirst
2021 J jnl
Completeness theorems for first-order logic analysed in constructive type theory.
J. Log. Comput.
Yannick Forster, Dominik Kirst, Dominik Wehr
2021 B conf
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq.
ITP
Dominik Kirst, Marc Hermes
2021 B conf
The generalised continuum hypothesis implies the axiom of choice in Coq.
CPP
Dominik Kirst, Felix Rech
2021 J jnl
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens.
CoRR
Dominik Kirst, Dominique Larchey-Wendling
2020 J jnl
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version).
CoRR
Yannick Forster, Dominik Kirst, Dominik Wehr
2020 Misc conf
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory.
LFCS
Yannick Forster, Dominik Kirst, Dominik Wehr
2020 — conf
Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory.
IJCAR (2)
Dominik Kirst, Dominique Larchey-Wendling
2020 J jnl
Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory.
CoRR
Dominik Kirst, Dominique Larchey-Wendling
2019 J jnl
Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory.
J. Autom. Reason.
Dominik Kirst, Gert Smolka
2019 B conf
On synthetic undecidability in coq, with an application to the entscheidungsproblem.
CPP
Yannick Forster, Dominik Kirst, Gert Smolka
2018 B conf
Large model constructions for second-order ZF in dependent type theory.
CPP
Dominik Kirst, Gert Smolka
2017 B conf
Categoricity Results for Second-Order ZF in Dependent Type Theory.
ITP
Dominik Kirst, Gert Smolka
2016 — conf
On the Verge: Voluntary Convergences for Accurate and Precise Timing of Gaze Input.
CHI Extended Abstracts
Dominik Kirst, Andreas Bulling