# A certifying extraction with time bounds from Coq to call-by-value λ-calculus

arXiv: https://arxiv.org/abs/1904.11818 · HTML: https://mlsanity.com/paper/1904.11818/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Apr 2019.

## Built on by (most cited first, 1 of 1)

- [Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens](https://mlsanity.com/paper/2104.14445/) (2021)

## Abstract (arXiv)

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 entirely written in Coq. We provide Ltac tactics to automatically verify the extracted terms w.r.t a logical relation connecting Coq functions with correct extractions and time bounds, essentially performing a certifying translation and running time validation. We provide three case studies: A universal L-term obtained as extraction from the Coq definition of a step-indexed self-interpreter for L, a many-reduction from solvability of Diophantine equations to the halting problem of L, and a polynomial-time simulation of Turing machines in L.