eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
17:1
17:19
10.4230/LIPIcs.ITP.2019.17
article
A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus
Forster, Yannick
1
Kunze, Fabian
1
Saarland University, Saarland Informatics Campus (SIC), Saarbrücken, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.17/LIPIcs.ITP.2019.17.pdf
call-by-value
lambda calculus
Coq
constructive type theory
extraction
computability