| 2026 | FSCD | Not Choosing Is Still a Choice: Constructive mathematics without any choice. | Martin Baillon, Yannick Forster, Dominik Kirst, Assia Mahboubi, Pierre-Marie Pdrot |
| 2025 | CSL | Completeness of First-Order Bi-Intuitionistic Logic. | Dominik Kirst, Ian Shillito |
| 2025 | FSCD | From Partial to Monadic: Combinatory Algebra with Effects. | Liron Cohen, Ariel Grunfeld, Dominik Kirst, tienne Miquey |
| 2025 | LICS | Syntactic Effectful Realizability in Higher-Order Logic. | Liron Cohen, Ariel Grunfeld, Dominik Kirst, tienne Miquey |
| 2025 | LICS | The Blurred Drinker Paradox: Constructive Reverse Mathematics of the Downward Lwenheim-Skolem Theorem. | Dominik Kirst, Haoyi Zeng |
| 2024 | CPP | A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic. | Ian Shillito, Dominik Kirst |
| 2024 | CSL | The Kleene-Post and Post's Theorem in the Calculus of Inductive Constructions. | Yannick Forster, Dominik Kirst, Niklas Mck |
| 2024 | LICS | Separating Markov's Principles. | Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, Vincent Rahli |
| 2023 | APLAS | Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions. | Yannick Forster, Dominik Kirst, Niklas Mck |
| 2023 | CSL | Gdel's Theorem Without Tears - Essential Incompleteness in Synthetic Computability. | Dominik Kirst, Benjamin Peters |
| 2022 | CPP | Undecidability, incompleteness, and completeness of second-order logic in Coq. | Mark Koch, Dominik Kirst |
| 2022 | FSCD | An Analysis of Tennenbaum's Theorem in Constructive Type Theory. | Marc Hermes, Dominik Kirst |
| 2022 | ITP | Undecidability of Dyadic First-Order Logic in Coq. | Johannes Hostert, Andrej Dudenhefner, Dominik Kirst |
| 2022 | ITP | Computational Back-And-Forth Arguments in Constructive Type Theory. | Dominik Kirst |
| 2022 | LFCS | Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic. | Christian Hagemeier, Dominik Kirst |
| 2022 | WoLLIC | Material Dialogues for First-Order Logic in Constructive Type Theory. | Dominik Wehr, Dominik Kirst |
| 2021 | CPP | The generalised continuum hypothesis implies the axiom of choice in Coq. | Dominik Kirst, Felix Rech |
| 2021 | ITP | Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. | Dominik Kirst, Marc Hermes |
| 2020 | CADE | Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory. | Dominik Kirst, Dominique Larchey-Wendling |
| 2020 | LFCS | Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory. | Yannick Forster, Dominik Kirst, Dominik Wehr |
| 2019 | CPP | On synthetic undecidability in coq, with an application to the entscheidungsproblem. | Yannick Forster, Dominik Kirst, Gert Smolka |
| 2018 | CPP | Large model constructions for second-order ZF in dependent type theory. | Dominik Kirst, Gert Smolka |
| 2017 | ITP | Categoricity Results for Second-Order ZF in Dependent Type Theory. | Dominik Kirst, Gert Smolka |
| 2016 | CHI | On the Verge: Voluntary Convergences for Accurate and Precise Timing of Gaze Input. | Dominik Kirst, Andreas Bulling |