Programming Systems Lab: Publications by Dominik Kirst

Saarland University Computer Science

Select author:

2021

Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq   (pdf)
Dominik Kirst, Marc Hermes
Interactive Theorem Proving - 12th International Conference, ITP 2021, Rome, Italy (To appear)

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