2 citations · 2 across the 1 of their papers we have counts for
2 papers
cs.LO2020★ 2 cited
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…
cs.LO2018
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…