17 citations · 23 across the 5 of their papers we have counts for
5 papers
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions
Yannick Forster, Dominik Kirst, Niklas Mück
We develop synthetic notions of oracle computability and Turing reducibility in the Calculus of Inductive Constructions (CIC), the constructive type theory underlying the Coq proof…
An Analysis of Tennenbaum's Theorem in Constructive Type Theory
Marc Hermes, Dominik Kirst
Tennenbaum's theorem states that the only countable model of Peano arithmetic (PA) with computable arithmetical operations is the standard model of natural numbers. In this paper,…
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens
Dominik Kirst, Dominique Larchey-Wendling
We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. Employing synthetic accounts of enumerability and decidability, we give a fu…
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)
Yannick Forster, Dominik Kirst, Dominik Wehr
We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the c…
Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory
Dominik Kirst, Dominique Larchey-Wendling
We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. Employing synthetic accounts of enumerability and decidability, we give a fu…