Follow
Dominik Kirst
Dominik Kirst
Postdoc, Ben-Gurion University
Verified email at ps.uni-saarland.de - Homepage
Title
Cited by
Cited by
Year
On synthetic undecidability in Coq, with an application to the Entscheidungsproblem
Y Forster, D Kirst, G Smolka
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019
762019
A Coq library of undecidable problems
Y Forster, D Larchey-Wendling, A Dudenhefner, E Heiter, D Kirst, F Kunze, ...
CoqPL 2020 The Sixth International Workshop on Coq for Programming Languages, 2020
452020
Completeness theorems for first-order logic analysed in constructive type theory: Extended version
Y Forster, D Kirst, D Wehr
Journal of Logic and Computation 31 (1), 112-151, 2021
332021
Synthetic undecidability and incompleteness of first-order axiom systems in Coq
D Kirst, M Hermes
12th International Conference on Interactive Theorem Proving (ITP 2021), 2021
27*2021
Trakhtenbrot’s theorem in Coq: a constructive approach to finite model theory
D Kirst, D Larchey-Wendling
Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris …, 2020
242020
Completeness theorems for first-order logic analysed in constructive type theory
Y Forster, D Kirst, D Wehr
International Symposium on Logical Foundations of Computer Science, 47-74, 2019
242019
On the verge: Voluntary convergences for accurate and precise timing of gaze input
D Kirst, A Bulling
Proceedings of the 2016 CHI Conference Extended Abstracts on Human Factors …, 2016
242016
A toolbox for mechanised first-order logic
J Hostert, M Koch, D Kirst
The Coq Workshop 2021, 2021
142021
Categoricity results for second-order ZF in dependent type theory
D Kirst, G Smolka
Interactive Theorem Proving: 8th International Conference, ITP 2017 …, 2017
142017
Categoricity results and large model constructions for second-order ZF in dependent type theory
D Kirst, G Smolka
Journal of Automated Reasoning 63, 415-438, 2019
132019
Large model constructions for second-order ZF in dependent type theory
D Kirst, G Smolka
Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018
132018
An Analysis of Tennenbaum's Theorem in Constructive Type Theory
M Hermes, D Kirst
Logical Methods in Computer Science 20, 2024
112024
A Coq library for mechanised first-order logic
D Kirst, J Hostert, A Dudenhefner, Y Forster, M Hermes, M Koch, ...
The Coq Workshop 2022, 2022
92022
Undecidability of dyadic first-order logic in Coq
J Hostert, A Dudenhefner, D Kirst
13th International Conference on Interactive Theorem Proving (ITP 2022), 2022
72022
Gödel’s theorem without tears-essential incompleteness in synthetic computability
D Kirst, B Peters
31st EACSL Annual Conference on Computer Science Logic (CSL 2023), 2023
62023
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens
D Kirst, D Larchey-Wendling
Logical Methods in Computer Science 18, 2022
52022
Undecidability, incompleteness, and completeness of second-order logic in Coq
M Koch, D Kirst
Proceedings of the 11th ACM SIGPLAN International Conference on Certified …, 2022
52022
Mechanised metamathematics: An investigation of first-order logic and set theory in constructive type theory
D Kirst
Saarländische Universitäts-und Landesbibliothek, 2022
52022
Synthetic versions of the kleene-post and post’s theorem
D Kirst, Y Forster, N Mück
28th International Conference on Types for Proofs and Programs (TYPES 2022), 2022
52022
Constructive and mechanised meta-theory of intuitionistic epistemic logic
C Hagemeier, D Kirst
Logical Foundations of Computer Science: International Symposium, LFCS 2022 …, 2022
52022
The system can't perform the operation now. Try again later.
Articles 1–20