5 citations · 11 across the 3 of their papers we have counts for
3 papers
cs.LO2019★ 5 cited
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…
cs.LO2018★ 3 cited
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…
cs.LO2016★ 3 cited
Towards the Integration of an Intuitionistic First-Order Prover into Coq
Fabian Kunze
An efficient intuitionistic first-order prover integrated into Coq is useful to replay proofs found by external automated theorem provers. We propose a two-phase approach: An intui…