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 categorical axiomatisations of second-order ZF.

**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, USA, 2018.

**Categoricity Results for Second-Order ZF in Dependent Type Theory** *(pdf)* *(slides)*

*Dominik Kirst and Gert Smolka*

ITP 2017, Brasilia, Brazil, 2017.

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

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

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

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

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

Summer 2017 | Advisor Category 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. |

Felix Rech, 2019, Master's thesis: On the Generalized Continuum Hypothesis in Coq

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

Formalising Completeness of First-Order Logic

Leonhard Staut, 2017, Bachelor's thesis: Nu-Trees in Coq

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

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

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