Program Optimisations via Hylomorphisms for Extraction of Executable Code
11 hours ago
- #program optimization
- #formal verification
- #hylomorphisms
- Generic programming with recursion schemes provides powerful abstractions for structuring recursion and reasoning about program optimizations.
- Formalizing recursion schemes in type theory offers termination guarantees but often compromises performance or requires unsafe casts.
- This paper presents the first Rocq formalization of hylomorphisms, enabling mechanization of all recognized recursive algorithms.
- The formalization is axiom-free and allows extraction of safe, idiomatic functional code.
- The framework is demonstrated with algorithms based on divide-and-conquer, dynamic programming, and mutual recursion.
- Extracted code is efficient, readable, and runnable.
- Machine-checked proofs of hylomorphism laws are used for program optimizations.