Document Open Access Logo

Program Optimisations via Hylomorphisms for Extraction of Executable Code

Authors David Castro Perez , Marco Paviotti , Michael Vollmer

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2025.32.pdf
  • Filesize: 0.72 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Functional constructs
  • Theory of computation → Type theory
  • Theory of computation → Program verification
Keywords
  • hylomorphisms
  • program calculation
  • divide and conquer
  • fusion

Metrics

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

Abstract

Generic programming with recursion schemes provides a powerful abstraction for structuring recursion and provides a rigorous reasoning principle for program optimisations which have been successfully applied to compilers for functional languages. Formalising recursion schemes in a type theory offers additional termination guarantees, but it often requires compromising on performance, requiring the assumption of additional axioms, and/or introducing unsafe casts into extracted code.
This paper presents the first Rocq formalisation of hylomorphisms allowing for the mechanisation of all recognised recursive algorithms. The key contribution of this paper is that this formalisation is fully axiom-free, and it allows the extraction of safe, idiomatic functional code. We exemplify the framework by formalising a series of algorithms based on different recursive paradigms such as divide-and conquer, dynamic programming, and mutual recursion and demonstrate that the extracted functional code for the programs formalised in our framework is efficient, humanly readable, and runnable. Furthermore, we show the use of the machine-checked proofs of the laws of hylomorphisms to do program optimisations.

Cite As Get BibTex

David Castro Perez, Marco Paviotti, and Michael Vollmer. Program Optimisations via Hylomorphisms for Extraction of Executable Code. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.32

Author Details

David Castro Perez
  • University Of Kent, Canterbury, UK
Marco Paviotti
  • University Of Kent, Canterbury, UK
Michael Vollmer
  • University Of Kent, Canterbury, UK

Funding

  • Castro Perez, David: EP/Y00339X/1, EP/T014512/1.

Supplementary Materials

References

  1. Michael Gordon Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theor. Comput. Sci., 342(1):3-27, 2005. URL: https://doi.org/10.1016/J.TCS.2005.06.002.
  2. Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, and Aaron Stump. A type-based approach to divide-and-conquer recursion in Coq. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571196.
  3. Jiří Adámek, Stefan Milius, and Lawrence S. Moss. On well-founded and recursive coalgebras. In Jean Goubault-Larrecq and Barbara König, editors, Foundations of Software Science and Computation Structures, pages 17-36, Cham, 2020. Springer International Publishing. Google Scholar
  4. Richard S. Bird and Oege de Moor. The algebra of programming. In Manfred Broy, editor, Proceedings of the NATO Advanced Study Institute on Deductive Program Design, Marktoberdorf, Germany, pages 167-203, 1996. Google Scholar
  5. Ana Bove, Alexander Krauss, and Matthieu Sozeau. Partiality and recursion in interactive theorem provers – an overview. Mathematical Structures in Computer Science, 26(1):38-88, 2016. URL: https://doi.org/10.1017/S0960129514000115.
  6. Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Recursive coalgebras from comonads. In Jirí Adámek and Stefan Milius, editors, Proceedings of the Workshop on Coalgebraic Methods in Computer Science, CMCS 2004, Barcelona, Spain, March 27-29, 2004, volume 106 of Electronic Notes in Theoretical Computer Science, pages 43-61. Elsevier, 2004. URL: https://doi.org/10.1016/J.ENTCS.2004.02.034.
  7. David Castro-Perez, Kevin Hammond, and Susmit Sarkar. Farms, pipes, streams and reforestation: reasoning about structured parallel processes using types and hylomorphisms. In Proc. of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, pages 4-17. ACM, 2016. URL: https://doi.org/10.1145/2951913.2951920.
  8. David Castro Perez, Marco Paviotti, and Michael Vollmer. dcastrop/coq-hylomorphisms. Software, EP/Y00339X/1, EP/T014512/1, (visited on 2025-09-03). URL: https://github.com/dcastrop/coq-hylomorphisms
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.23907
  9. Nils Anders Danielsson, John Hughes, Patrik Jansson, and Jeremy Gibbons. Fast and loose reasoning is morally correct. In J. Gregory Morrisett and Simon L. Peyton Jones, editors, Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, pages 206-217. ACM, 2006. URL: https://doi.org/10.1145/1111037.1111056.
  10. Eleanor Davies and Sara Kalvala. Postcondition-preserving fusion of postorder tree transformations. In Proceedings of the 29th International Conference on Compiler Construction, CC 2020, pages 191-200, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3377555.3377884.
  11. Yannick Forster, Matthieu Sozeau, and Nicolas Tabareau. Verified Extraction from Coq to OCaml. working paper or preprint, November 2023. URL: https://inria.hal.science/hal-04329663.
  12. Jeremy Gibbons. The third homomorphism theorem. Journal of Functional Programming, 6(4):657-665, 1996. Earlier version appeared in C. B. Jay, editor, Computing: The Australian Theory Seminar, Sydney, December 1994, p. 62-69. URL: https://doi.org/10.1017/S0956796800001908.
  13. Jeremy Gibbons. The school of squiggol. In Formal Methods. FM 2019 International Workshops, pages 35-53, Cham, 2020. Springer International Publishing. Google Scholar
  14. Andy Gill and Graham Hutton. The worker/wrapper transformation. Journal of Functional Programming, 19, March 2009. URL: https://doi.org/10.1017/S0956796809007175.
  15. Ralf Hinze, Thomas Harper, and Daniel W. H. James. Theory and practice of fusion. In Jurriaan Hage and Marco T. Morazán, editors, Implementation and Application of Functional Languages - 22nd International Symposium, IFL 2010, Alphen aan den Rijn, The Netherlands, September 1-3, 2010, Revised Selected Papers, volume 6647 of Lecture Notes in Computer Science, pages 19-37. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-24276-2_2.
  16. Ralf Hinze, Nicolas Wu, and Jeremy Gibbons. Conjugate hylomorphisms - or: The mother of all structured recursion schemes. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 527-538. ACM, 2015. URL: https://doi.org/10.1145/2676726.2676989.
  17. Graham Hutton, Mauro Jaskelioff, and Andy Gill. Factorising folds for faster functions. J. Funct. Program., 20(3–4):353-373, July 2010. URL: https://doi.org/10.1017/S0956796810000122.
  18. Chantal Keller and Marc Lasson. Parametricity in an Impredicative Sort. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, volume 16 of Leibniz International Proceedings in Informatics (LIPIcs), pages 381-395, Dagstuhl, Germany, 2012. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.381.
  19. Dominique Larchey-Wendling and Jean-François Monin. The Braga method: Extracting certified algorithms from complex recursive schemes in Coq. In PROOF AND COMPUTATION II: From Proof Theory and Univalent Mathematics to Program Extraction and Verification, pages 305-386. World Scientific, 2022. Google Scholar
  20. Marino Miculan and Marco Paviotti. Synthesis of distributed mobile programs using monadic types in Coq. In Lennart Beringer and Amy P. Felty, editors, Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, volume 7406 of Lecture Notes in Computer Science, pages 183-200. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_13.
  21. Akimasa Morihata, Kiminori Matsuzaki, Zhenjiang Hu, and Masato Takeichi. The third homomorphism theorem on trees: downward & upward lead to divide-and-conquer. In Zhong Shao and Benjamin C. Pierce, editors, Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, pages 177-185. ACM, 2009. URL: https://doi.org/10.1145/1480881.1480905.
  22. Shin-Cheng Mu, Hsiang-Shang Ko, and Patrik Jansson. Algebra of programming in agda: Dependent types for relational program derivation. J. Funct. Program., 19(5):545-579, 2009. URL: https://doi.org/10.1017/S0956796809007345.
  23. Kosuke Murata and Kento Emoto. Recursion schemes in Coq. In Anthony Widjaja Lin, editor, Programming Languages and Systems, pages 202-221, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-34175-6_11.
  24. Laith Sakka, Kirshanthan Sundararajah, and Milind Kulkarni. Treefuser: a framework for analyzing and fusing general recursive tree traversals. Proc. ACM Program. Lang., 1(OOPSLA), October 2017. URL: https://doi.org/10.1145/3133900.
  25. Neil Sculthorpe and Graham Hutton. Work it, wrap it, fix it, fold it. Journal of Functional Programming, 24(1):113-127, 2014. URL: https://doi.org/10.1017/S0956796814000045.
  26. Matthieu Sozeau. Program-ing finger trees in Coq. In Ralf Hinze and Norman Ramsey, editors, Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, October 1-3, 2007, pages 13-24. ACM, 2007. URL: https://doi.org/10.1145/1291151.1291156.
  27. Matthieu Sozeau. A new look at generalized rewriting in type theory. J. Formaliz. Reason., 2(1):41-62, 2009. URL: https://doi.org/10.6092/ISSN.1972-5787/1574.
  28. Matthieu Sozeau and Cyprien Mangin. Equations reloaded: high-level dependently-typed functional programming and proving in Coq. Proc. ACM Program. Lang., 3(ICFP):86:1-86:29, 2019. URL: https://doi.org/10.1145/3341690.
  29. Akihiko Takano and Erik Meijer. Shortcut deforestation in calculational form. In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, FPCA '95, pages 306-313, New York, NY, USA, 1995. Association for Computing Machinery. URL: https://doi.org/10.1145/224164.224221.
  30. Julien Tesson, Hideki Hashimoto, Zhenjiang Hu, Frédéric Loulergue, and Masato Takeichi. Program calculation in Coq. In Michael Johnson and Dusko Pavlovic, editors, Algebraic Methodology and Software Technology, pages 163-179, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  31. Philip Wadler. Deforestation: Transforming programs to eliminate trees. Theor. Comput. Sci., 73(2):231-248, 1990. URL: https://doi.org/10.1016/0304-3975(90)90147-A.
  32. Glynn Winskel and Mogens Nielsen. Models for concurrency. In Handbook of Logic in Computer Science. Oxford University Press, May 1995. URL: https://doi.org/10.1093/oso/9780198537809.003.0001.
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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact