Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
From MaRDI portal
Publication:3434629
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
This page was built for publication: Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
