| 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 | 66 | 2019 |
| 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 | 40 | 2020 |
| 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 | 24 | 2021 |
| 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 | 20 | 2016 |
| 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 | 19 | 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 | 19 | 2020 |
| 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 | 16 | 2020 |
| Categoricity results for second-order ZF in dependent type theory D Kirst, G Smolka Interactive Theorem Proving: 8th International Conference, ITP 2017 …, 2017 | 12 | 2017 |
| 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 | 11 | 2018 |
| A toolbox for mechanised first-order logic J Hostert, M Koch, D Kirst The Coq Workshop 2021, 2021 | 10 | 2021 |
| 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 | 9 | 2019 |
| An analysis of Tennenbaum’s theorem in constructive type theory M Hermes, D Kirst 7th International Conference on Formal Structures for Computation and …, 2022 | 4 | 2022 |
| 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 | 2 | 2022 |
| Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens D Larchey-Wendling, D Kirst Logical Methods in Computer Science 18, 2022 | 2 | 2022 |
| 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 | 2 | 2022 |
| Computational Back-And-Forth Arguments in Constructive Type Theory D Kirst 13th International Conference on Interactive Theorem Proving (ITP 2022), 2022 | 2 | 2022 |
| Undecidability of dyadic first-order logic in Coq J Hostert, A Dudenhefner, D Kirst 13th International Conference on Interactive Theorem Proving (ITP 2022), 2022 | 1 | 2022 |
| Strong, synthetic, and computational proofs of Gödel’s first incompleteness theorem B Peters, D Kirst TYPES, 2022 | 1 | 2022 |
| Constructive and Mechanised Meta-theory of Intuitionistic Epistemic Logic C Hagemeier, D Kirst Logical Foundations of Computer Science: International Symposium, LFCS 2022 …, 2022 | 1 | 2022 |
| Towards Extraction of Continuity Moduli in Coq Y Forster, D Kirst, F Steinberg EUTYPES-TYPES 2020, 2020 | 1 | 2020 |
Gert SmolkaProfessor of Computer Science, Saarland University, Saarland Informatics CampusVerified email at ps.uni-saarland.de
