DROPS

Artifact

Software

dcastrop/coq-hylomorphisms

Authors: David Castro Perez, Marco Paviotti, and Michael Vollmer

Abstract

Cite as

David Castro Perez, Marco Paviotti, Michael Vollmer. dcastrop/coq-hylomorphisms (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-23907,
   title = {{dcastrop/coq-hylomorphisms}}, 
   author = {Castro Perez, David and Paviotti, Marco and Vollmer, Michael},
   note = {Software, EP/Y00339X/1, EP/T014512/1, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:72a5871702972010658c8b75970475a540abf44d;origin=https://github.com/dcastrop/coq-hylomorphisms;visit=swh:1:snp:3033a9703c61e14e58b51c7f66c784b9955e737f;anchor=swh:1:rev:305c425fdd165254bbf1bee47ed9d44d6b93fa3c}{\texttt{swh:1:dir:72a5871702972010658c8b75970475a540abf44d}} (visited on 2025-09-22)},
   url = {https://github.com/dcastrop/coq-hylomorphisms},
   doi = {10.4230/artifacts.23907},
}

Document

DOI: 10.4230/LIPIcs.ITP.2025.32

Program Optimisations via Hylomorphisms for Extraction of Executable Code

Authors: David Castro Perez, Marco Paviotti, and Michael Vollmer

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

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

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)

Copy BibTex To Clipboard

@InProceedings{castroperez_et_al:LIPIcs.ITP.2025.32,
  author =	{Castro Perez, David and Paviotti, Marco and Vollmer, Michael},
  title =	{{Program Optimisations via Hylomorphisms for Extraction of Executable Code}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{32:1--32:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.32},
  URN =		{urn:nbn:de:0030-drops-246302},
  doi =		{10.4230/LIPIcs.ITP.2025.32},
  annote =	{Keywords: hylomorphisms, program calculation, divide and conquer, fusion}
}

Search Results

Documents authored by Castro Perez, David

dcastrop/coq-hylomorphisms

Abstract

Cite as

Program Optimisations via Hylomorphisms for Extraction of Executable Code

Abstract

Cite as

Thanks for your feedback!

Could not send message