Follow
Dominik Kirst
Dominik Kirst
PhD Student, Saarland 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
662019
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
402020
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
242021
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
202016
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
192021
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
192020
Completeness theorems for first-order logic analysed in constructive type theory
Y Forster, D Kirst, D Wehr
Logical Foundations of Computer Science: International Symposium, LFCS 2020 …, 2020
162020
Categoricity results for second-order ZF in dependent type theory
D Kirst, G Smolka
Interactive Theorem Proving: 8th International Conference, ITP 2017 …, 2017
122017
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
112018
A toolbox for mechanised first-order logic
J Hostert, M Koch, D Kirst
The Coq Workshop 2021, 2021
102021
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
92019
An analysis of Tennenbaum’s theorem in constructive type theory
M Hermes, D Kirst
7th International Conference on Formal Structures for Computation and …, 2022
42022
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
22022
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens
D Larchey-Wendling, D Kirst
Logical Methods in Computer Science 18, 2022
22022
Synthetic versions of the Kleene-Post and Post’s theorem
D Kirst, N Mück, Y Forster
28th International Conference on Types for Proofs and Programs (TYPES 2022), 2022
22022
Computational Back-And-Forth Arguments in Constructive Type Theory
D Kirst
13th International Conference on Interactive Theorem Proving (ITP 2022), 2022
22022
Undecidability of dyadic first-order logic in Coq
J Hostert, A Dudenhefner, D Kirst
13th International Conference on Interactive Theorem Proving (ITP 2022), 2022
12022
Strong, synthetic, and computational proofs of Gödel’s first incompleteness theorem
B Peters, D Kirst
TYPES, 2022
12022
Constructive and Mechanised Meta-theory of Intuitionistic Epistemic Logic
C Hagemeier, D Kirst
Logical Foundations of Computer Science: International Symposium, LFCS 2022 …, 2022
12022
Towards Extraction of Continuity Moduli in Coq
Y Forster, D Kirst, F Steinberg
EUTYPES-TYPES 2020, 2020
12020
The system can't perform the operation now. Try again later.
Articles 1–20