Dominik Kirst

Orcid: 0000-0003-4126-6975

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

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
An Analysis of Tennenbaum's Theorem in Constructive Type Theory.
Log. Methods Comput. Sci., 2024

Separating Markov's Principles.
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.
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.
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.
J. Autom. Reason., March, 2023

Gödel's Theorem Without Tears - Essential Incompleteness in Synthetic Computability.
Proceedings of the 31st EACSL Annual Conference on Computer Science Logic, 2023

Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions.
Proceedings of the Programming Languages and Systems - 21st Asian Symposium, 2023

2022
Constructive and mechanised meta-theory of IEL and similar modal logics.
J. Log. Comput., 2022

Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens.
Log. Methods Comput. Sci., 2022

Material Dialogues for First-Order Logic in Constructive Type Theory.
Proceedings of the Logic, Language, Information, and Computation, 2022

Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic.
Proceedings of the Logical Foundations of Computer Science - International Symposium, 2022

Computational Back-And-Forth Arguments in Constructive Type Theory.
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Undecidability of Dyadic First-Order Logic in Coq.
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Undecidability, incompleteness, and completeness of second-order logic in Coq.
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.
J. Log. Comput., 2021

The generalised continuum hypothesis implies the axiom of choice in Coq.
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).
CoRR, 2020

Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory.
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.
J. Autom. Reason., 2019

On synthetic undecidability in coq, with an application to the entscheidungsproblem.
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.
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.
Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

2016
On the Verge: Voluntary Convergences for Accurate and Precise Timing of Gaze Input.
Proceedings of the 2016 CHI Conference on Human Factors in Computing Systems, 2016


  Loading...