Hi, I'm Dominik and I'm a MSCA Postdoctoral Fellow hosted by Hugo Herbelin in the Picube Team part of IRIF and Inria Paris. Before that, I was a Minerva Postdoctoral Fellow hosted by Liron Cohen at Ben-Gurion University and a PhD student at the Saarbrücken Graduate School of Computer Science under the supervision of Gert Smolka.
I did my Bachelor's Thesis and a Research Immersion Lab on set theory mechanised in Coq. I obtained my Master's degree from the University of Oxford with a thesis on intersection type systems and nominal automata. I also completed a second Bachelor's degree in cultural studies with a thesis on foundations of mathematics, hosted by the philosophy department. In my PhD thesis I investigated various topics in metamathematics in constructive type theory and Coq.
I'm broadly interested in constructive and computational logic and its connections to the foundations and philosophy of mathematics. My active lines of work are concerned with effectful realisability, synthetic oracle computability, bi-intuitionistic logic, computational incompleteness proofs, and the constructive reverse mathematics of completeness theorems.
From Partial to Monadic: Combinatory Algebra with Effects
Liron Cohen, Ariel Grunfeld, Dominik Kirst, Étienne Miquey
FSCD 2025, Birmingham, UK, 2025.
The Blurred Drinker Paradox: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem
Dominik Kirst, Haoyi Zeng
LICS 2025, Singapore, 2025.
Syntactic Effectful Realizability in Higher-Order Logic
Liron Cohen, Ariel Grunfeld, Dominik Kirst, Étienne Miquey, Ross Tate
LICS 2025, Singapore, 2025.
Completeness of First-Order Bi-intuitionistic Logic (pdf)
Dominik Kirst, Ian Shillito
CSL 2025, Amsterdam, Netherlands, 2025.
Separating Markov's Principles (pdf)
Liron Cohen, Yannick Forster, Dominik Kirst, Bruno Da Rocha Paiva, Vincent Rahli
LICS 2024, Tallinn, Estonia, 2024.
An Analysis of Tennenbaum's Theorem in Constructive Type Theory (Extended Version) (pdf)
Marc Hermes, Dominik Kirst
Logical Methods in Computer Science, 2024.
A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-Intuitionistic Logic (pdf)
Ian Shillito, Dominik Kirst
CPP 2024, London, UK, 2024.
The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions (pdf)(slides)
Yannick Forster, Dominik Kirst, Niklas Mück
CSL 2024, Naples, Italy, 2024.
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions (pdf)
Yannick Forster, Dominik Kirst, Niklas Mück
APLAS 2023, Taipei, Taiwan, 2023.
Material Dialogues for First-Order Logic in Constructive Type Theory (Extended Version) (pdf)
Dominik Wehr, Dominik Kirst
Mathematical Structures in Computer Science, 2023.
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq (Extended Version) (pdf)
Dominik Kirst, Marc Hermes
Journal of Automated Reasoning, 2023.
Gödel's Theorem Without Tears: Essential Incompleteness in Synthetic Computability (pdf)(slides)
Dominik Kirst, Benjamin Peters
CSL 2023, Warsaw, Poland, 2023.
Constructive and Mechanised Meta-Theory of IEL and Similar Modal Logics (pdf)
Christian Hagemeier, Dominik Kirst
Journal of Logic and Computation, 2022
Material Dialogues for First-Order Logic in Constructive Type Theory (pdf)
Dominik Wehr, Dominik Kirst
WoLLIC 2022, Iaşi, Romania, 2022.
An Analysis of Tennenbaum's Theorem in Constructive Type Theory (pdf)
Marc Hermes, Dominik Kirst
Best paper award by junior researchers
FSCD 2022, Haifa, Israel, 2022.
Computational Back-and-Forth Arguments in Constructive Type Theory (pdf)(slides)
Dominik Kirst
ITP 2022, Haifa, Israel, 2022.
Undecidability of Dyadic First-Order Logic in Coq (pdf)
Johannes Hostert, Andrej Dudenhefner, Dominik Kirst
ITP 2022, Haifa, Israel, 2022.
Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq (pdf)(slides)(video)
Mark Koch, Dominik Kirst
CPP 2022, Philadelphia, Pennsylvania, USA, 2022.
Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic (pdf)(slides)(video)
Christian Hagemeier, Dominik Kirst
LFCS 2022, Deerfield Beach, Florida, USA, 2022.
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens (pdf)
Dominik Kirst, Dominique Larchey-Wendling
Logical Methods in Computer Science, 2022.
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq (pdf)(slides)(video)
Dominik Kirst, Marc Hermes
ITP 2021, Rome, Italy, 2021.
The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq (pdf)(slides)(video)
Dominik Kirst, Felix Rech
CPP 2021, Copenhagen, Denmark, 2021.
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version) (pdf)
Yannick Forster, Dominik Kirst, Dominik Wehr
Journal of Logic and Computation, 2021
Trakhtenbrot's Theorem in Coq: A Constructive Approach to Finite Model Theory (pdf)(slides)(video)
Dominik Kirst, Dominique Larchey-Wendling
IJCAR 2020, Paris, France, 2020.
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (pdf)(slides)
Yannick Forster, Dominik Kirst, Dominik Wehr
LFCS 2020, Deerfield Beach, Florida, USA, 2020.
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem (pdf)(slides)
Yannick Forster, Dominik Kirst, Gert Smolka
CPP 2019, Cascais, Portugal, 2019.
Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory (pdf)
Dominik Kirst and Gert Smolka
Journal of Automated Reasoning, 2018.
Large Model Constructions for Second-Order ZF in Dependent Type Theory (pdf)(slides)
Dominik Kirst and Gert Smolka
CPP 2018, Los Angeles, California, USA, 2018.
Categoricity Results for Second-Order ZF in Dependent Type Theory (pdf)(slides)
Dominik Kirst and Gert Smolka
ITP 2017, Brasilia, Brazil, 2017.
A Succinct and Verified Completeness Proof for First-Order Bi-Intuitionistic Logic (pdf)
Dominik Kirst, Ian Shillito
Meeting of the Australasian Association for Logic, Sydney, Australia, 2024.
Post's Problem in Constructive Mathematics (pdf)(slides)
Haoyi Zeng, Yannick Forster, Dominik Kirst, Takako Nemoto