Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant

DOI10.1007/11737414_9zbMath1185.68616OpenAlexW2097281451MaRDI QIDQ3434629

David Pichardie, Vlad Rusu, Julien Forest, Gilles Barthe

Publication date: 2 May 2007

Published in: Functional and Logic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11737414_9

Mathematics Subject Classification ID

Related Items (13)

Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques ⋮ A formally verified compiler back-end ⋮ Extraction in Coq: An Overview ⋮ Unnamed Item ⋮ Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves ⋮ A Short Presentation of Coq ⋮ Mechanically certifying formula-based Noetherian induction reasoning ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion ⋮ A formalization of convex polyhedra based on the simplex method ⋮ Another Look at Function Domains ⋮ Termination of Isabelle Functions via Termination of Rewriting

Uses Software

• Coq
• Isabelle/HOL
• PVS
• CoLoR

This page was built for publication: Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant