Document Open Access Logo

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

Authors Dominique Larchey-Wendling, Jean-François Monin



PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.21.pdf
  • Filesize: 0.65 MB
  • 17 pages

Document Identifiers

Author Details

Dominique Larchey-Wendling
  • Université de Lorraine, CNRS, LORIA, Vandœuvre-lès-Nancy, France
Jean-François Monin
  • Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, France

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.ITP.2023.21

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Type theory
  • Theory of computation → Functional constructs
  • Software and its engineering → Formal methods
  • Software and its engineering → Functional languages
  • Theory of computation → Higher order logic
Keywords
  • Unbounded linear search
  • μ-recursive functions
  • computational contents
  • Coq
  • extraction
  • OCaml

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. George S. Boolos, John P. Burgess, and Richard C. Jeffrey. Computability and Logic. Cambridge University Press, 4 edition, 2002. URL: https://doi.org/10.1017/CBO9781139164931.
  2. Mario Carneiro. Formalizing Computability Theory via Partial Recursive Functions. In ITP 2019, volume 141, pages 12:1-12:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.12.
  3. Robert L. Constable et al. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, NJ, 1986. Google Scholar
  4. Yannick Forster. Church’s Thesis and Related Axioms in Coq’s Type Theory. In CSL 2021, volume 183, pages 21:1-21:19. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.21.
  5. Yannick Forster. Parametric church’s thesis: Synthetic computability without choice. In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, pages 70-89, Cham, 2022. Springer International Publishing. Google Scholar
  6. Susumu Hayashi. Extracting Lisp Programs from Constructive Proofs: A Formal Theory of Constructive Mathematic Based on Lisp, volume 19, pages 169-191. Publications of the Research Institute for Mathematical Sciences, 1983. Google Scholar
  7. Stephen C. Kleene. λ-definability and recursiveness. Duke Mathematical Journal, 2(2):340-353, 1936. URL: https://doi.org/10.1215/S0012-7094-36-00227-2.
  8. Stephen C. Kleene. Recursive predicates and quantifiers. Trans. Amer. Math. Soc., 53:43-73, 1943. URL: https://doi.org/10.1090/S0002-9947-1943-0007371-8.
  9. Dominique Larchey-Wendling. Typing Total Recursive Functions in Coq. In ITP 2017, pages 371-388. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_24.
  10. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s Tenth Problem in Coq (Extended Version). Logical Methods in Computer Science, Volume 18, Issue 1:35:1-35:41, March 2022. URL: https://doi.org/10.46298/lmcs-18(1:35)2022.
  11. Dominique Larchey-Wendling and Jean-François Monin. The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq, chapter 8, pages 305-386. World Scientific, 2021. URL: https://doi.org/10.1142/9789811236488_0008.
  12. Joseph R. Shoenfield. Mathematical Logic. Addison-Wesley series in logic. Addison-Wesley, 1967. Google Scholar
  13. Vincent Zammit. A Proof of the S-m-n theorem in Coq. Technical report, The Computing Laboratory, The University of Kent, Canterbury, Kent, UK, March 1997. URL: http://kar.kent.ac.uk/21524/.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail