The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq

DOI10.1142/9789811236488_0008MaRDI QIDQ5081874zbMATH OpenOpenAlexFDO

Authors Dominique Larchey-Wendling, Jean-François Monin

Publication date 17 June 2022

Published in Proof and Computation II (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-03338785/file/the_braga_method.pdf

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX) General logic (03Bxx) Computability and recursion theory (03Dxx) Proof theory and constructive mathematics (03Fxx)

Recommendations

• scientific article; zbMATH DE number 2003158
• Synthesis of ML programs in the system Coq
• Developing certified programs in the system Coq the program tactic
• Verifying programs in the calculus of inductive constructions
• Simple general recursion in type theory

Cited in

(4)

• Braga Method
• Recursion schemes in Coq
• Mechanised uniform interpolation for modal logics K, GL, and iSL
• Program optimisations via hylomorphisms for extraction of executable code

Describes a project that uses

Uses Software

• OCaml
• CompCert
• Coq

This page was built for publication: The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq

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