2 citations · 2 across the 3 of their papers we have counts for
4 papers · 1 filter
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…
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…
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…