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. Currently, I'm mostly working on synthetic computability and constructive reverse mathematics, both using the Coq proof assistant.

**Completeness of First-Order Bi-intuitionistic Logic**

*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 Dompleteness Proof for First-Order Bi-Intuitionistic Logic** *(pdf)*

*Dominik Kirst, Ian Shillito*

Meeting of the Australasian Association for Logic, Sydney, Australia, 2024.

**Mechanised Constructive Reverse Mathematics:Completeness, Löwenheim-Skolem Theorem, Post’s Problem**

LIX Proofs and Algorithms Seminar, Paris-Saclay, France, 2024.

**Separating Markov's Principles:An Introduction to Constructive Reverse Mathematics**

CHoCoLa Meeting, Lyon, France, 2024.

**Post's Problem in Constructive Mathematics** *(pdf)(slides)*

*Haoyi Zeng, Yannick Forster, Dominik Kirst, Takako Nemoto*

Continuity, Computability, Constructivity Workshop, Nice, France, 2024.

**Constructive Reverse Mathematics of the Downwards Löwenheim-Skolem Theorem** *(pdf)(slides)*

*Dominik Kirst, Haoyi Zeng*

Logic Colloquium 2024, Gothenburg, Sweden, 2024.

**The Blurred Drinker Paradox and Blurred Choice Axioms
for the Downward Löwenheim-Skolem Theorem** *(pdf)*

*Dominik Kirst, Haoyi Zeng*

Types 2024, Copenhagen, Denmark, 2024.

**Limited Principles of Omniscience in Constructive Type Theory** *(pdf)*

*Bruno da Rocha Paiva, Liron Cohen, Yannick Forster, Dominik Kirst, Vincent Rahli*

Types 2024, Copenhagen, Denmark, 2024.

**Post’s Problem and the Priority Method in CIC** *(pdf)*

*Haoyi Zeng, Yannick Forster, Dominik Kirst*

Types 2024, Copenhagen, Denmark, 2024.

**Mechanised Constructive Reverse Mathematics:Soundness and Completeness of Bi-Intuitionistic Logic**

Australasian Logic Colloquium 2023, Brisbane, Australia, 2023.

**New Observations on the Constructive Content of First-Order Completeness Theorems** *(pdf)(slides)*

*Hugo Herbelin, Dominik Kirst*

Types 2023, Valencia, Spain, 2023.

**Markov's Principles in Constructive Type Theory** *(pdf)*

*Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, Vincent Rahli*

Types 2023, Valencia, Spain, 2023.

**Constructive and Mechanised Meta-Theory of IEL and Similar Modal Logics** *(slides)*

*Christian Hagmeier, Dominik Kirst*

CUNY Computational Logic Seminar, New York City/Online, 2022.

**A Coq Library for Mechanised First-Order Logic** *(pdf)(slides)*

*Dominik Kirst, Johannes Hostert, Andrej Dudenhefner, Yannick Forster, Marc Hermes, Mark Koch, Dominique Larchey-Wendling, Niklas Mück, Benjamin Peters, Gert Smolka, Dominik Wehr*

The Coq Workshop, Haifa, Israel, 2022.

**Strong, Synthetic, and Computational Proofs of Gödel's First Incompleteness Theorem** *(pdf)*

*Benjamin Peters, Dominik Kirst*

Types 2022, Nantes, France, 2022.

**Synthetic Versions of the Kleene-Post and Post's Theorem** *(pdf)(slides)*

*Dominik Kirst, Niklas Mück, Yannick Forster*

Types 2022, Nantes, France, 2022.

**Synthetic Turing Reducibility in CIC** *(pdf)*

*Yannick Forster, Dominik Kirst*

Types 2022, Nantes, France, 2022.

**A Feasible Formalisation of Incompleteness** *(demo)*

Formalize!(?) - 2, Zurich/Online, 2022.

**Analysing First-Order Logic in Constructive Type Theory** *(slides)*

*Dominik Kirst, Dominik Wehr, Yannick Forster*

ANU Logic Seminar, Canberra/Online, 2021.

**Formalising Metamathematics in Constructive Type Theory** *(slides)*

Autumn School Proof and Computation, Online, 2021.

**The Generalised Continuum Hypothesis Implies the Axiom of Choice in HoTT** *(pdf)(slides)(video)*

*Dominik Kirst, Felix Rech*

Workshop on Homotopy Type Theory / Univalent Foundations, Buenos Aires, Argentina, 2021.

**A Toolbox for Mechanised First-Order Logic** *(pdf)(slides)(video)*

*Johannes Hostert, Mark Koch, Dominik Kirst*

The Coq Workshop, Rome, Italy, 2021.

**Synthetic Undecidability Proofs in Coq** *(slides)*

Computer Science Theory Seminar, Tallinn, Estonia, 2020.

**Towards Extraction of Continuity Moduli in Coq** *(pdf)(slides)*

*Yannick Forster, Dominik Kirst, Florian Steinberg*

Types 2020, Turin, Italy, 2020.

**A Coq Library of Undecidable Problems** *(pdf)*

*Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, Maximilian Wuttke*

CoqPL 2020, New Orleans, USA, 2020.

**Mechanised Metamathematics:An Investigation of First-Order Logic and Set Theory in Constructive Type Theory**

PhD Thesis, Programming Systems Lab, Saarland University, 2022.

**Foundations of Mathematics: A Discussion of Sets and Types** *(pdf)*

*Dominik Kirst*

Bachelor's Thesis, Department of Philosophy, Saarland University, 2018.

**Intersection Type Systems Corresponding to Nominal Automata** *(pdf)*

*Dominik Kirst*

Master's Thesis, Lady Margaret Hall, University of Oxford, 2016.

**Formalised Set Theory: Well-Orderings and the Axiom of Choice** *(pdf)*

*Dominik Kirst*

Bachelor's Thesis, Programming Systems Lab, Saarland University, 2014.

Janis Bailitis, 2023, Bachelor's thesis, co-advised with Yannick Forster:

Löb's Theorem in Coq

Fabian Brenner, 2023, Bachelor's thesis, co-advised with Yannick Forster:

The undecidability of finitary PCF in Coq

Haoyi Zeng, 2023, Bachelor's thesis, co-advised with Yannick Forster:

Post's Problem and the Priority Method

Yannic Muskalla, 2021, Bachelor's thesis, co-advised with Holger Sturm:

Translating Intuitionistic Modal Logic to Classical Bimodal Logic in Coq

Benjamin Peters, 2021, Bachelor's thesis:

Computational Proofs of Gödel's First Incompleteness Theorem in Coq

Niklas Mück, 2021, Bachelor's thesis, co-advised with Yannick Forster:

The Arithmetical Hierarchy and Post’s Theorem in Coq

Mark Koch, 2021, Bachelor's thesis:

Mechanization of Second-order Logic

Johannes Hostert, 2021, Bachelor's thesis, co-advised with Andrej Dudenhefner:

The Undecidability of First-order Logic over Small Signatures

Christian Hagemeier, 2020, Bachelor's thesis, co-advised with Holger Sturm:

Formalizing Intuitonistic Epistemic Logic in Coq

Marc Hermes, 2020, Master's thesis, co-advised with Moritz Weber:

Formalisation of Peano Arithmetic in Coq

Felix Rech, 2019, Master's thesis:

On the Generalized Continuum Hypothesis in Coq

Dominik Wehr, 2019, Bachelor's thesis, co-advised with Yannick Forster:

Formalising Completeness of First-Order Logic

Leonhard Staut, 2017, Bachelor's thesis:

Nu-Trees in Coq

Winter 2023/2024 | LecturerANU Logic Summer School Advanced Course, School of Computing. |

Winter 2021/2022 | Teaching AssistantProgramming 1 Basic Course, Programming Systems Lab. |

Winter 2020/2021 | AdvisorAdvanced Coq Programming Advanced Course, Programming Systems Lab. |

Summer 2020 | Teaching AssistantIntroduction to Computational Logic Core Course, Programming Systems Lab. |

Summer 2020 | AdvisorFunktionale Programmierung Proseminar, Programming Systems Lab. |

Summer 2019 | Teaching AssistantIntroduction to Computational Logic Core Course, Programming Systems Lab. |

Winter 2018/2019 | Organiser, Advisor, and LecturerFoundations of Mathematics Seminar, Programming Systems Lab. |

Winter 2018/2019 | CoachMathematics Precourse Saarland University. |

Summer 2018 | Teaching AssistantIntroduction to Computational Logic Core Course, Programming Systems Lab. |

Summer 2018 | AdvisorAdvanced Coq Programming Advanced Course, Programming Systems Lab. |

Winter 2017/2018 | Advisor Category Theory Seminar, Programming Systems Lab. |

Summer 2017 | Advisor and LecturerCategory Theory Seminar, Programming Systems Lab. |

Summer 2014 | Student TAIntroduction to Computational Logic Core Course, Programming Systems Lab. |

Winter 2013/2014 | Student TATheoretical Computer ScienceBasic Course, Programming Systems Lab. |

Summer 2013 | Student TAProgramming 2Basic Course, Compiler Design Lab. |

Winter 2012/2013 | Student TAProgramming 1 Basic Course, Programming Systems Lab. |

Summer 2012 | Student TAMathematics Precourse Saarland University. |

Mail: | kirst at cs.uni-saarland.de |

Adress: | Saarland University, Saarland Informatics Campus E1 3, Rm 523 66123 Saarbrücken |

Phone: | +49 (0)681 / 302-5626 |