research
∙
07/28/2023
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions
We develop synthetic notions of oracle computability and Turing reducibi...
share
research
∙
02/28/2023
An Analysis of Tennenbaum's Theorem in Constructive Type Theory
Tennenbaum's theorem states that the only countable model of Peano arith...
research
∙
04/29/2021
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens
We study finite first-order satisfiability (FSAT) in the constructive se...
research
∙
06/08/2020
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)
We study various formulations of the completeness of first-order logic p...
research
∙
04/15/2020
