Programming Systems Lab: Publications by Dominik Kirst

Saarland University Computer Science

Select author:

2023

Gödel's Theorem Without Tears: Essential Incompleteness in Synthetic Computability   (pdf)
Dominik Kirst, Benjamin Peters
Computer Science Logic (CSL'23), Warsaw, Poland

2022

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.

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

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

2020

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.

2019

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

2018

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

2017

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


Login to edit


Legal notice, Privacy policy