Dominik Kirst

According to our database, Dominik Kirst authored at least 23 papers between 2016 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

An Analysis of Tennenbaum's Theorem in Constructive Type Theory.

Marc Hermes, Dominik Kirst

Log. Methods Comput. Sci., 2024

Separating Markov's Principles.

Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, Vincent Rahli

Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, 2024

The Kleene-Post and Post's Theorem in the Calculus of Inductive Constructions.

Yannick Forster, Dominik Kirst, Niklas Mück

Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic, 2024

A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic.

Ian Shillito, Dominik Kirst

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2023

Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq.

Dominik Kirst, Marc Hermes

J. Autom. Reason., March, 2023

Gödel's Theorem Without Tears - Essential Incompleteness in Synthetic Computability.

Dominik Kirst, Benjamin Peters

Proceedings of the 31st EACSL Annual Conference on Computer Science Logic, 2023

Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions.

Yannick Forster, Dominik Kirst, Niklas Mück

Proceedings of the Programming Languages and Systems - 21st Asian Symposium, 2023

2022

Constructive and mechanised meta-theory of IEL and similar modal logics.

Christian Hagemeier, Dominik Kirst

J. Log. Comput., 2022

Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens.

Dominik Kirst, Dominique Larchey-Wendling

Log. Methods Comput. Sci., 2022

Material Dialogues for First-Order Logic in Constructive Type Theory.

Dominik Wehr, Dominik Kirst

Proceedings of the Logic, Language, Information, and Computation, 2022

Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic.

Christian Hagemeier, Dominik Kirst

Proceedings of the Logical Foundations of Computer Science - International Symposium, 2022

Computational Back-And-Forth Arguments in Constructive Type Theory.

Dominik Kirst

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Undecidability of Dyadic First-Order Logic in Coq.

Johannes Hostert, Andrej Dudenhefner, Dominik Kirst

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Undecidability, incompleteness, and completeness of second-order logic in Coq.

Mark Koch, Dominik Kirst

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

2021

Completeness theorems for first-order logic analysed in constructive type theory.

Yannick Forster, Dominik Kirst, Dominik Wehr

J. Log. Comput., 2021

The generalised continuum hypothesis implies the axiom of choice in Coq.

Dominik Kirst, Felix Rech

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020

Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version).

Yannick Forster, Dominik Kirst, Dominik Wehr

CoRR, 2020

Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory.

Dominik Kirst, Dominique Larchey-Wendling

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory.

Dominik Kirst, Gert Smolka

J. Autom. Reason., 2019

On synthetic undecidability in coq, with an application to the entscheidungsproblem.

Yannick Forster, Dominik Kirst, Gert Smolka

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018

Large model constructions for second-order ZF in dependent type theory.

Dominik Kirst, Gert Smolka

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017

Categoricity Results for Second-Order ZF in Dependent Type Theory.

Dominik Kirst, Gert Smolka

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

2016

On the Verge: Voluntary Convergences for Accurate and Precise Timing of Gaze Input.

Dominik Kirst, Andreas Bulling

Proceedings of the 2016 CHI Conference on Human Factors in Computing Systems, 2016