LIPIcs.ITP.2019.17.pdf
- Filesize: 0.63 MB
- 19 pages
Document
A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus
Authors
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2019-09-05
Cite AsGet BibTex
Yannick Forster and Fabian Kunze. A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 17:1-17:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.17
https://doi.org/10.4230/LIPIcs.ITP.2019.17
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Type theory
- Mathematics of computing → Lambda calculus
Keywords
- call-by-value
- lambda calculus
- Coq
- constructive type theory
- extraction
- computability
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads