Dominik Kirst

Saarland University Computer Science
Dominik Kirst

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.


Research Papers

Trakhtenbrot's Theorem in Coq: A Constructive Approach to Finite Model Theory (pdf)
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.


Extened Abstracts

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.


Theses

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.


Teaching

Summer 2020 Teaching Assistant
Introduction to Computational Logic
Core Course, Programming Systems Lab.
Summer 2020 Advisor
Funktionale Programmierung
Proseminar, Programming Systems Lab.
Summer 2019 Teaching Assistant
Introduction to Computational Logic
Core Course, Programming Systems Lab.
Winter 2018/2019 Organiser, Advisor, and Lecturer
Foundations of Mathematics
Seminar, Programming Systems Lab.
Winter 2018/2019 Coach
Mathematics Precourse
Saarland University.
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 and Lecturer
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.

Supervised Students

Marc Hermes, 2020, Master's thesis (ongoing), co-advised with Moritz Weber:
Formalisation of Peano Arithmetic in Coq

Felix Rech, 2019, Master's thesis (ongoing):
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


Contact

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


Legal notice, Privacy policy