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.
@InProceedings{forster_et_al:LIPIcs.ITP.2019.17, author = {Forster, Yannick and Kunze, Fabian}, title = {{A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {17:1--17:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.17}, URN = {urn:nbn:de:0030-drops-110724}, doi = {10.4230/LIPIcs.ITP.2019.17}, annote = {Keywords: call-by-value, lambda calculus, Coq, constructive type theory, extraction, computability} }
Feedback for Dagstuhl Publishing