My name is Dominik and I am a PhD student at the Saarbrücken Graduate School of Computer Science and the Programming Systems Lab.

I did my Bachelor's Thesis and a Research Immersion Lab on set theory formalised in Coq. I obtained my Master's degree from the University of Oxford with a thesis on intersection type systems and nominal automata. I recently finished a second Bachelor's degree in cultural studies with a thesis on foundations of mathematics hosted by the philosophy department.

I am broadly interested in computational logic and its connections to the foundations and philosophy of mathematics. Currently, I am working on mechanised first-order logic and categorical axiomatisations of second-order ZF.

**Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens** *(pdf)*

* Dominik Kirst, Dominique Larchey-Wendling*

Submitted for review.

**Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq** *(pdf)*

* 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.

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

*Dominik Kirst, Felix Rech*

Submitted for review.

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

*Johannes Hostert, Mark Koch, Dominik Kirst*

Submitted for review.

**Synthetic Undecidability Proofs in Coq:
Entscheidungsproblem, Trakhtenbrotâ€™s Theorem, First-Order Axiom Systems**

Talk at the 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.

**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.

Mark Koch, 2021, Bachelor's thesis (ongoing):

Mechanization of Second-order Logic

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

The Undecidability of First-order Logic over Small Signatures

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

Formalizing Intuitonistic Epistemic Logic in Coq

Marc Hermes, 2020, Master's thesis (ongoing), 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 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: | dominik.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 |