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

DOI10.1142/9789811236488_0008OpenAlexW3188171585MaRDI QIDQ5081874

Jean-François Monin, Dominique Larchey-Wendling

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

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

Related Items (1)

Braga Method

Uses Software

• Coq
• OCaml
• CompCert

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