A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus

Yannick Forster, Fabian Kunze

We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value $\lambda$-calculus L. The plugin is implemented in the MetaCoq framework and entir…