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
∙
12/22/2021
Parametric Church's Thesis: Synthetic Computability without Choice
In synthetic computability, pioneered by Richman, Bridges, and Bauer, on...
research
∙
09/01/2020
Church's thesis and related axioms in Coq's type theory
"Church's thesis" (𝖢𝖳) as an axiom in constructive logic states that eve...
research
∙
06/25/2020
Generating induction principles and subterm relations for inductive types using MetaCoq
We implement three Coq plugins regarding inductive types in MetaCoq. The...
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
∙
03/10/2020
Hilbert's Tenth Problem in Coq
We formalise the undecidability of solvability of Diophantine equations,...
research
∙
04/26/2019
A certifying extraction with time bounds from Coq to call-by-value λ-calculus
We provide a plugin extracting Coq functions of simple polymorphic types...
research
∙
02/20/2019
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space
We study the weak call-by-value λ-calculus as a model for computational ...
research
∙
06/08/2018
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine
We formally verify an abstract machine for a call-by-value lambda-calcul...
research
∙
11/19/2017