Proof pearl: constructive extraction of cycle finding algorithms

DOI10.1007/978-3-319-94821-8_22OpenAlexW2810357523MaRDI QIDQ1791179

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

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

Uses Software

• Coq
• OCaml
• Tortoise Hare

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