An Analysis of Tennenbaum's Theorem in Constructive Type Theory
(pdf)
Marc Hermes, Dominik Kirst
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), Haifa, Israel
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq
(pdf)
Dominik Kirst, Marc Hermes
12th International Conference on Interactive Theorem Proving (ITP 2021)