
Church's thesis and related axioms in Coq's type theory
"Church's thesis" (π’π³) as an axiom in constructive logic states that eve...
read it

Generating induction principles and subterm relations for inductive types using MetaCoq
We implement three Coq plugins regarding inductive types in MetaCoq. The...
read it

Completeness Theorems for FirstOrder Logic Analysed in Constructive Type Theory (Extended Version)
We study various formulations of the completeness of firstorder logic p...
read it

Hilbert's Tenth Problem in Coq
We formalise the undecidability of solvability of Diophantine equations,...
read it

A certifying extraction with time bounds from Coq to callbyvalue Ξ»calculus
We provide a plugin extracting Coq functions of simple polymorphic types...
read it

The Weak CallByValue Ξ»Calculus is Reasonable for Both Time and Space
We study the weak callbyvalue Ξ»calculus as a model for computational ...
read it

Formal Smallstep Verification of a Callbyvalue Lambda Calculus Machine
We formally verify an abstract machine for a callbyvalue lambdacalcul...
read it

Verification of PCPRelated Computational Reductions in Coq
We formally verify several computational reductions concerning the Post ...
read it
Yannick Forster
is this you? claim profile