Gödel's Theorem Without Tears: Essential Incompleteness in Synthetic Computability
(pdf)
Dominik Kirst, Benjamin Peters
Computer Science Logic (CSL'23), Warsaw, Poland
An Analysis of Tennenbaum's Theorem in Constructive Type Theory
(pdf)
Marc Hermes, Dominik Kirst
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), Haifa, Israel
Computational Back-and-Forth Arguments in Constructive Type Theory
(pdf)
Dominik Kirst
13th International Conference on Interactive Theorem Proving (ITP 2022), Haifa, Israel
Undecidability of Dyadic First-Order Logic in Coq
(pdf)
Johannes Hostert, Andrej Dudenhefner, Dominik Kirst
13th International Conference on Interactive Theorem Proving (ITP 2022), Haifa, Israel
Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq
(pdf)
Mark Koch, Dominik Kirst
Certified Programs and Proofs (CPP), January 17-18, 2022, Philadelphia, Pennsylvania, U.S.A.
Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic
(pdf)
Christian Hagemeier, Dominik Kirst
Logical Foundations of Computer Science (LFCS), January 10-13, 2022, Deerfield Beach, Florida, U.S.A.
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
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq
(pdf)
Dominik Kirst, Marc Hermes
12th International Conference on Interactive Theorem Proving (ITP 2021)
The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq
(pdf)
Dominik Kirst, Felix Rech
10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, Copenhagen, Denmark
Trakhtenbrot's Theorem in Coq: A Constructive Approach to Finite Model Theory
(pdf)
Dominik Kirst, Dominique Larchey-Wendling
International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory
(pdf)
Yannick Forster, Dominik Kirst, Dominik Wehr
Symposium on Logical Foundations Of Computer Science (LFCS 2020), January 4-7, 2020, Deerfield Beach, Florida, U.S.A.
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
(pdf)
Yannick Forster, Dominik Kirst, Gert Smolka
8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019
Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory
(pdf)
Dominik Kirst, Gert Smolka
Journal of Automated Reasoning
Large Model Constructions for Second-Order ZF in Dependent Type Theory
(pdf)
Dominik Kirst, Gert Smolka
Certified Programs and Proofs - 7th International Conference, CPP 2018, Los Angeles, USA, January 8-9, 2018
Categoricity Results for Second-Order ZF in Dependent Type Theory
(pdf)
Dominik Kirst, Gert Smolka
Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017