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

TL;DR

This paper presents a Coq plugin that extracts functions to a call-by-value lambda calculus, verifies their correctness and time bounds, and demonstrates its effectiveness through three case studies involving interpreters, solvability, and Turing machine simulation.

Contribution

It introduces a certifying extraction method from Coq to lambda calculus with automatic verification of correctness and time bounds, implemented within the MetaCoq framework.

Findings

Successfully extracted a self-interpreter for \\L with time bounds.

Reduced Diophantine solvability to halting problem in L.

Simulated Turing machines in polynomial time within L.

Abstract

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 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.