Document Open Access Logo

A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus

Authors Yannick Forster, Fabian Kunze

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.17.pdf
  • Filesize: 0.63 MB
  • 19 pages

Document Identifiers

Author Details

Yannick Forster
  • Saarland University, Saarland Informatics Campus (SIC), Saarbrücken, Germany
Fabian Kunze
  • Saarland University, Saarland Informatics Campus (SIC), Saarbrücken, Germany

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

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)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. CertiCoq: A verified compiler for Coq. In The Third International Workshop on Coq for Programming Languages (CoqPL), 2017. Google Scholar
  2. Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. Towards Certified Meta-Programming with Typed Template-Coq. In International Conference on Interactive Theorem Proving, pages 20-39. Springer, 2018. Google Scholar
  3. Andrea Asperti and Wilmer Ricciotti. A formalization of multi-tape Turing machines. Theoretical Computer Science, 603:23-42, October 2015. URL: https://doi.org/10.1016/j.tcs.2015.07.013.
  4. Andrej Bauer. First steps in synthetic computability theory. Electronic Notes in Theoretical Computer Science, 155:5-31, 2006. Google Scholar
  5. Simon Pierre Boulier. Extending type theory with syntactic models. PhD thesis, Ecole nationale supérieure Mines-Télécom Atlantique, 2018. Google Scholar
  6. Yannick Forster, Edith Heiter, and Gert Smolka. Verification of PCP-Related Computational Reductions in Coq. arXiv preprint arXiv:1711.07023, 2017. Accepted at ITP 2018. Google Scholar
  7. Yannick Forster, Dominik Kirst, and Gert Smolka. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 38-51. ACM, 2019. Google Scholar
  8. Yannick Forster and Fabian Kunze. Verified Extraction from Coq to a Lambda-Calculus. Coq Workshop 2016, 2016. Google Scholar
  9. Yannick Forster, Fabian Kunze, and Marc Roth. The weak call-by-value λ-calculus is reasonable for both time and space. CoRR, abs/1902.07515, 2019. URL: http://arxiv.org/abs/1902.07515.
  10. Yannick Forster and Dominique Larchey-Wendling. Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic. In Workshop on Syntax and Semantics of Low-level Languages, Oxford, 2018. Google Scholar
  11. Yannick Forster and Dominique Larchey-Wendling. Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 104-117. ACM, 2019. Google Scholar
  12. Yannick Forster and Gert Smolka. Weak call-by-value lambda calculus as a model of computation in Coq. In ITP 2017, pages 189-206. Springer, 2017. Google Scholar
  13. Armaël Guéneau, Arthur Charguéraud, and François Pottier. A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification. In European Symposium on Programming, pages 533-560. Springer, 2018. Google Scholar
  14. Lars Hupel and Tobias Nipkow. A verified compiler from Isabelle/HOL to CakeML. In European Symposium on Programming, pages 999-1026. Springer, 2018. Google Scholar
  15. Jan Martin Jansen. Programming in the λ-Calculus: From Church to Scott and Back. In The Beauty of Functional Code, volume 8106 of LNCS, pages 168-180. Springer, 2013. Google Scholar
  16. Nils Köpp. Automatically verified program extraction from proofs with applications to constructive analysis. Master’s thesis, LMU Munich, 2018. URL: http://www.mathematik.uni-muenchen.de/~schwicht/seminars/semws18/main.pdf.
  17. Ramana Kumar, Magnus O Myreen, Michael Norrish, and Scott Owens. CakeML: a verified implementation of ML. In ACM SIGPLAN Notices, volume 49, pages 179-191. ACM, 2014. Google Scholar
  18. Fabian Kunze, Gert Smolka, and Yannick Forster. Formal Small-step Verification of a Call-by-value Lambda Calculus Machine. In Asian Symposium on Programming Languages and Systems, pages 264-283. Springer, 2018. Google Scholar
  19. Ugo Dal Lago and Simone Martini. The weak lambda calculus as a reasonable machine. Theor. Comput. Sci., 398(1-3):32-50, 2008. URL: https://doi.org/10.1016/j.tcs.2008.01.044.
  20. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s Tenth Problem in Coq. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 27:1-27:20, 2019. Google Scholar
  21. Pierre Letouzey. Certified functional programming: program extraction within Coq proof assistant. PhD thesis, Université Paris-Sud, France, 2004. Google Scholar
  22. Gregory Michael Malecha. Extensible proof engineering in intensional type theory. Harvard University, 2015. Google Scholar
  23. Torben Æ. Mogensen. Efficient Self-Interpretations in lambda Calculus. J. Funct. Program., 2(3):345-363, 1992. URL: https://doi.org/10.1017/S0956796800000423.
  24. Eric Mullen, Stuart Pernsteiner, James R Wilcox, Zachary Tatlock, and Dan Grossman. Œuf: minimizing the Coq extraction TCB. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 172-185. ACM, 2018. Google Scholar
  25. Magnus O Myreen and Scott Owens. Proof-producing translation of higher-order logic into pure and stateful ML. Journal of Functional Programming, 24(2-3):284-315, 2014. Google Scholar
  26. Gordon D. Plotkin. Call-by-Name, Call-by-Value and the lambda-Calculus. Theor. Comput. Sci., 1(2):125-159, 1975. URL: https://doi.org/10.1016/0304-3975(75)90017-1.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact