DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2023.21

Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq

Authors: Dominique Larchey-Wendling and Jean-François Monin

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract

Basing on an original Coq implementation of unbounded linear search for partially decidable predicates, we study the computational contents of μ-recursive functions via their syntactic representation, and a correct by construction Coq interpreter for this abstract syntax. When this interpreter is extracted, we claim the resulting OCaml code to be the natural combination of the implementation of the μ-recursive schemes of composition, primitive recursion and unbounded minimization of partial (i.e., possibly non-terminating) functions. At the level of the fully specified Coq terms, this implies the representation of higher-order functions of which some of the arguments are themselves partial functions. We handle this issue using some techniques coming from the Braga method. Hence we get a faithful embedding of μ-recursive algorithms into Coq preserving not only their extensional meaning but also their intended computational behavior. We put a strong focus on the quality of the Coq artifact which is both self contained and with a line of code count of less than 1k in total.

Cite as

Dominique Larchey-Wendling and Jean-François Monin. Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{larcheywendling_et_al:LIPIcs.ITP.2023.21,
  author =	{Larchey-Wendling, Dominique and Monin, Jean-Fran\c{c}ois},
  title =	{{Proof Pearl: Faithful Computation and Extraction of \mu-Recursive Algorithms in Coq}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.21},
  URN =		{urn:nbn:de:0030-drops-183963},
  doi =		{10.4230/LIPIcs.ITP.2023.21},
  annote =	{Keywords: Unbounded linear search, \mu-recursive functions, computational contents, Coq, extraction, OCaml}
}

Search Results

Documents authored by Monin, Jean-François

Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq

Abstract

Cite as

Thanks for your feedback!

Could not send message