| 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 | 73 | 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 | 45 | 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 | 32 | 2021 |
| Synthetic undecidability and incompleteness of first-order axiom systems in Coq D Kirst, M Hermes Saarländische Universitäts-und Landesbibliothek, 2023 | 24 | 2023 |
| 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 | 24 | 2020 |
| 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 | 22 | 2019 |
| 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 | 22 | 2016 |
| A toolbox for mechanised first-order logic J Hostert, M Koch, D Kirst The Coq Workshop 2021, 2021 | 14 | 2021 |
| Categoricity results for second-order ZF in dependent type theory D Kirst, G Smolka Interactive Theorem Proving: 8th International Conference, ITP 2017 …, 2017 | 14 | 2017 |
| 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 | 13 | 2019 |
| 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 | 13 | 2018 |
| An Analysis of Tennenbaum's Theorem in Constructive Type Theory M Hermes, D Kirst arXiv preprint arXiv:2302.14699, 2023 | 10 | 2023 |
| 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 | 8 | 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 | 6 | 2022 |
| 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 | 5 | 2023 |
| 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 | 5 | 2022 |
| Constructive and mechanised meta-theory of intuitionistic epistemic logic C Hagemeier, D Kirst Logical Foundations of Computer Science: International Symposium, LFCS 2022 …, 2022 | 5 | 2022 |
| Synthetic undecidability and incompleteness of first-order axiom systems in Coq: Extended version D Kirst, M Hermes Journal of Automated Reasoning 67 (1), 13, 2023 | 4 | 2023 |
| Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens D Kirst, D Larchey-Wendling Logical Methods in Computer Science 18, 2022 | 4 | 2022 |
| 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 | 4 | 2022 |
Yannick ForsterCambium Team, Inria ParisVerified email at inria.fr
