Dominik Kirst

Programming Systems

Dominik Kirst

Bachelor's Thesis

Research Immersion Lab

Master's Thesis

2nd Bachelor's Thesis

PhD Thesis

My name is Dominik and I'm 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 also completed a second Bachelor's degree in cultural studies with a thesis on foundations of mathematics hosted by the philosophy department. I've recently submitted my PhD thesis.

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 mechanised first-order logic and categorical axiomatisations of second-order ZF, both using the Coq proof assistant.

Research Papers

Gödel's Theorem Without Tears: Essential Incompleteness in Synthetic Computability (pdf)
Dominik Kirst, Benjamin Peters
Submitted for review.

Constructive and Mechanised Meta-Theory of IEL and Similar Modal Logics (pdf)
Christian Hagemeier, Dominik Kirst
Submitted for review.

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.

Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq (Extended Version) (pdf)
Dominik Kirst, Marc Hermes
Journal of Automated Reasoning, to appear.

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.

Extended Abstracts and Talks

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.

Formalising Metamathematics in Constructive Type Theory (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.

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.

Supervised Students

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

Teaching

Contact