| Publication | Date of Publication | Type |
|---|
| Completeness of first-order bi-intuitionistic logic | 2026-06-09 | Paper |
| The Kleene-Post and Post's theorem in the calculus of inductive constructions | 2026-02-19 | Paper |
| Separating Markov's principles | 2025-06-18 | Paper |
Material dialogues for first-order logic in constructive type theory: extended version
Mathematical Structures in Computer Science | 2024-11-29 | Paper |
| Gödel's theorem without tears -- essential incompleteness in synthetic computability | 2024-09-25 | Paper |
| Undecidability of dyadic first-order logic in Coq | 2024-07-15 | Paper |
| Computational back-and-forth arguments in constructive type theory | 2024-07-15 | Paper |
An analysis of Tennenbaum's theorem in constructive type theory
Logical Methods in Computer Science | 2024-06-27 | Paper |
| An analysis of Tennenbaum's theorem in constructive type theory | 2024-05-27 | Paper |
| Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions | 2023-07-28 | Paper |
| Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq | 2023-06-20 | Paper |
Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version
Journal of Automated Reasoning | 2023-06-14 | Paper |
Material dialogues for first-order logic in constructive type theory
Logic, Language, Information, and Computation | 2023-06-02 | Paper |
Constructive and mechanised meta-theory of IEL and similar modal logics
Journal Of Logic And Computation | 2023-01-04 | Paper |
Trakhtenbrot’s Theorem in Coq
Automated Reasoning | 2022-11-09 | Paper |
scientific article; zbMATH DE number 7566073 (Why is no real title available?)
(available as arXiv preprint) | 2022-08-02 | Paper |
| scientific article; zbMATH DE number 7566073 (Why is no real title available?) | 2022-08-02 | Paper |
| Constructive and mechanised meta-theory of intuitionistic epistemic logic | 2022-07-01 | Paper |
Completeness theorems for first-order logic analysed in constructive type theory
Journal Of Logic And Computation | 2022-02-08 | Paper |
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens
(available as arXiv preprint) | 2021-04-29 | Paper |
Completeness theorems for first-order logic analysed in constructive type theory
(available as arXiv preprint) | 2020-05-06 | Paper |
Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory
(available as arXiv preprint) | 2020-04-15 | Paper |
Categoricity results and large model constructions for second-order ZF in dependent type theory
Journal of Automated Reasoning | 2019-08-21 | Paper |
| Categoricity results for second-order ZF in dependent type theory | 2018-01-04 | Paper |
An Analysis of Tennenbaum's Theorem in Constructive Type Theory
(available as arXiv preprint) | N/A | Paper |
