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 culutural 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 Assistant Introduction to Computational Logic Core Course, Programming Systems Lab. |
| Winter 2018/2019 | Organiser and Lecturer Foundations of Mathematics Seminar, Programming Systems Lab. |
| Summer 2018 | Teaching Assistant Introduction 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 TA Introduction to Computational Logic Core Course, Programming Systems Lab. |
| Winter 2013/2014 | Student TA Theoretical Computer Science Basic Course, Programming Systems Lab. |
| Summer 2013 | Student TA Programming 2 Basic Course, Compiler Design Lab. |
| Winter 2012/2013 | Student TA Programming 1 Basic Course, Programming Systems Lab. |
| Summer 2012 | Student TA Mathematics 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 |