Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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

Yannick Forster, Fabian Kunze

Interactive Theorem Proving - 10th International Conference, ITP 2019, Portland, USA, pp. 17:1–17:19, Schloss Dagstuhl--Leibniz-Zentrum für Informatik, April 2019

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.

Link to Coq plugin and formalisation - Also available at arXiv

Download PDF        Show BibTeX               

@CONFERENCE{ForsterKunze:2019:Certifying-extraction,
  title = {A certifying extraction with time bounds from Coq to call-by-value λ-calculus},
  author = {Yannick Forster and Fabian Kunze},
  year = {2019},
  month = {Apr},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
  booktitle = { Interactive Theorem Proving - 10th International Conference, ITP 2019, Portland, USA},
  pages = {17:1–17:19},
  note = {Also available as arXiv:1904.11818},
}

Login to edit