Sciweavers

Share
FLOPS
2006
Springer

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

8 years 9 months ago
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
Abstract. We present a practical tool for defining and proving properties of recursive functions in the Coq proof assistant. The tool generates from pseudo-code the graph of the intended function as an inductive relation. Then it proves that the relation actually represents a function, which is by construction the function that we are trying to define. Then, we generate induction and inversion principles, and a fixpoint equation for proving other properties of the function. Our tool builds upon stateof-the-art techniques for defining recursive functions, and can also be used to generate executable functions from inductive descriptions of their graph. We illustrate the benefits of our tool on two case studies.
Gilles Barthe, Julien Forest, David Pichardie, Vla
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where FLOPS
Authors Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu
Comments (0)
books