Castro-Perez, David, Paviotti, Marco, Vollmer, Michael (2024) Mechanising Recursion Schemes with Magic-Free Coq Extraction. In: Mechanising Recursion Schemes with Magic-Free Coq Extraction. . (In press) (doi:10.4230/LIPIcs.CVIT.2016.23) (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided) (KAR id:105615)
PDF
Author's Accepted Manuscript
Language: English Restricted to Repository staff only |
|
Contact us about this Publication
|
![]() |
Official URL: https://doi.org/10.4230/LIPIcs.CVIT.2016.23 |
Abstract
Generic programming with recursion schemes provides a powerful abstraction for structuring recursion while ensuring termination and providing reasoning about program equivalences, as well as deriving optimisations which have been successfully applied to functional programming. Formalising recursion schemes in a type theory offers additional termination guarantees, but it often requires compromises affecting the resulting code, such as imposing performance penalties, requiring the assumption of additional axioms, or introducing unsafe casts into extracted code (e.g. Obj.magic in OCaml). To the best of our knowledge, this paper presents the first Coq formalisation of a recursion scheme, called the hylomorphism, along with its algebraic laws allowing for the mechanisation of all recognised (terminating) recursive algorithms. The key contribution of this paper is that this formalisation is fully axiom-free allowing for the extraction of safe, idiomatic OCaml 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 OCaml code for the programs formalised in our framework is efficient, resembles code that a human programmer would write, and contains no occurrences of Obj.magic. We also present a machine-checked proof of the well-known short-cut fusion optimisation.
Item Type: | Conference or workshop item (UNSPECIFIED) |
---|---|
DOI/Identification number: | 10.4230/LIPIcs.CVIT.2016.23 |
Uncontrolled keywords: | hylomorphisms, Coq, code extraction, verification |
Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Funders: | University of Kent (https://ror.org/00xkeyj56) |
Depositing User: | Marco Paviotti |
Date Deposited: | 13 Apr 2024 11:46 UTC |
Last Modified: | 24 Apr 2024 10:04 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/105615 (The current URI for this page, for reference purposes) |
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):