18 citations · 52 across the 11 of their papers we have counts for
11 papers
Determination of the fifth Busy Beaver value
The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs +17
The Busy Beaver value is the maximum number of steps that an -state 2-symbol Turing machine can perform from the all-zero tape before halting. was historically introd…
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…
Parametric Church's Thesis: Synthetic Computability without Choice
Yannick Forster
In synthetic computability, pioneered by Richman, Bridges, and Bauer, one develops computability theory without an explicit model of computation. This is enabled by assuming an axi…
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…
A certifying extraction with time bounds from Coq to call-by-value -calculus
Yannick Forster, Fabian Kunze
We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value -calculus L. The plugin is implemented in the MetaCoq framework and entir…
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine
Fabian Kunze, Gert Smolka, Yannick Forster
We formally verify an abstract machine for a call-by-value lambda-calculus with de Bruijn terms, simple substitution, and small-step semantics. We follow a stepwise refinement appr…
Verification of PCP-Related Computational Reductions in Coq
Yannick Forster, Edith Heiter, Gert Smolka
We formally verify several computational reductions concerning the Post correspondence problem (PCP) using the proof assistant Coq. Our verifications include a reduction of a strin…
On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control
Yannick Forster, Ohad Kammar, Sam Lindley +1
We compare the expressive power of three programming abstractions for user-defined computational effects: Bauer and Pretnar's effect handlers, Filinski's monadic reflection, and de…