18 citations · 52 across the 11 of their papers we have counts for
4 papers · 1 filter
Church's thesis and related axioms in Coq's type theory
Yannick Forster
"Church's thesis" () as an axiom in constructive logic states that every total function of type is computable, i.e. definable in a model of…
Generating induction principles and subterm relations for inductive types using MetaCoq
Bohdan Liesnikov, Marcel Ullrich, Yannick Forster
We implement three Coq plugins regarding inductive types in MetaCoq. The first plugin is a simple syntax transformation generating alternative constructors for inductive types by a…
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…
Hilbert's Tenth Problem in Coq (Extended Version)
Dominique Larchey-Wendling, Yannick Forster
We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq's constructive type theory. To do so, we give the fi…