On the Verge: Voluntary Convergences for Accurate and Precise Timing of Gaze Input. - Dominik Kirst; Andreas Bulling (CHI Extended Abstracts, 2016)

Categoricity Results for Second-Order ZF in Dependent Type Theory. - Dominik Kirst; Gert Smolka (ITP, 2017)

Large model constructions for second-order ZF in dependent type theory. - Dominik Kirst; Gert Smolka (CPP, 2018)

On synthetic undecidability in coq, with an application to the entscheidungsproblem. - Yannick Forster 002; Dominik Kirst; Gert Smolka (CPP, 2019)

Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory. - Dominik Kirst; Gert Smolka (J. Autom. Reason., 2019)

Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory. - Dominik Kirst; Dominique Larchey-Wendling (IJCAR (2), 2020)

Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version). - Yannick Forster 002; Dominik Kirst; Dominik Wehr (CoRR, 2020)

The generalised continuum hypothesis implies the axiom of choice in Coq. - Dominik Kirst; Felix Rech (CPP, 2021)

Completeness theorems for first-order logic analysed in constructive type theory. - Yannick Forster 002; Dominik Kirst; Dominik Wehr (J. Log. Comput., 2021)

Undecidability, incompleteness, and completeness of second-order logic in Coq. - Mark Koch; Dominik Kirst (CPP, 2022)

Undecidability of Dyadic First-Order Logic in Coq. - Johannes Hostert; Andrej Dudenhefner; Dominik Kirst (ITP, 2022)

Computational Back-And-Forth Arguments in Constructive Type Theory. - Dominik Kirst (ITP, 2022)

Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic. - Christian Hagemeier; Dominik Kirst (LFCS, 2022)

Material Dialogues for First-Order Logic in Constructive Type Theory. - Dominik Wehr; Dominik Kirst (WoLLIC, 2022)

Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens. - Dominik Kirst; Dominique Larchey-Wendling (Log. Methods Comput. Sci., 2022)

Constructive and mechanised meta-theory of IEL and similar modal logics. - Christian Hagemeier; Dominik Kirst (J. Log. Comput., 2022)

Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions. - Yannick Forster 002; Dominik Kirst; Niklas Mück (APLAS, 2023)

Gödel's Theorem Without Tears - Essential Incompleteness in Synthetic Computability. - Dominik Kirst; Benjamin Peters (CSL, 2023)

Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. - Dominik Kirst; Marc Hermes (J. Autom. Reason., 2023)

A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic. - Ian Shillito; Dominik Kirst (CPP, 2024)

The Kleene-Post and Post's Theorem in the Calculus of Inductive Constructions. - Yannick Forster 002; Dominik Kirst; Niklas Mück (CSL, 2024)

Separating Markov's Principles. - Liron Cohen 001; Yannick Forster 002; Dominik Kirst; Bruno da Rocha Paiva; Vincent Rahli (LICS, 2024)

An Analysis of Tennenbaum's Theorem in Constructive Type Theory. - Marc Hermes; Dominik Kirst (Log. Methods Comput. Sci., 2024)

Material dialogues for first-order logic in constructive type theory: extended version. - Dominik Wehr; Dominik Kirst (Math. Struct. Comput. Sci., 2024)

Completeness of First-Order Bi-Intuitionistic Logic. - Dominik Kirst; Ian Shillito (CSL, 2025)

From Partial to Monadic: Combinatory Algebra with Effects. - Liron Cohen 001; Ariel Grunfeld; Dominik Kirst; Étienne Miquey (FSCD, 2025)

Syntactic Effectful Realizability in Higher-Order Logic. - Liron Cohen 001; Ariel Grunfeld; Dominik Kirst; Étienne Miquey (CoRR, 2025)