Proof pearl: constructive extraction of cycle finding algorithms

DOI10.1007/978-3-319-94821-8_22MaRDI QIDQ1791179zbMATH OpenOpenAlexFDO

Authors Dominique Larchey-Wendling

Publication date 4 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-94821-8_22

zbMATH Keywords

cycle findingbar inductive predicatescorrectness by extractionpartial algorithms in Coq

Mathematics Subject Classification ID

Graph algorithms (graph-theoretic aspects) (05C85) Paths and cycles (05C38) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Extraction and verification of programs by analysis of formal proofs
• scientific article; zbMATH DE number 2063221
• scientific article; zbMATH DE number 1973215
• Writing constructive proofs yielding efficient extracted programs
• The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction

Describes a project that uses

Uses Software

• Tortoise Hare
• OCaml
• Coq

This page was built for publication: Proof pearl: constructive extraction of cycle finding algorithms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1791179)