flop-barthe-forest-pichardie-rusu-06

G. Barthe, J. Forest, D. Pichardie, V. Rusu. Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In Functional and LOgic Programming Systems (FLOPS'06), LNCS, Volume 3945, Pages 114-129, Fuji Susono, Japan, April 2006.

Download [help]

Download paper: Doi page

Download paper: Adobe portable document (pdf)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

We present a practical tool for defining and proving properties of recursive functions in the Coq proof assistant. The tool proceeds by generating from pseudo-code (Coq functions that need not be total nor terminating) the graph of the intended function as an inductive relation, and then 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 state-of-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

Contact

Vlad Rusu http://www.irisa.fr/vertecs/Equipe/Rusu/vlad-rusu.html

BibTex Reference

@InProceedings{flop-barthe-forest-pichardie-rusu-06,
   Author = {Barthe, G. and Forest, J. and Pichardie, D. and Rusu, V.},
   Title = {Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant},
   BookTitle = {Functional and LOgic Programming Systems (FLOPS'06)},
   Volume = {3945},
   Pages = {114--129},
   Series = {LNCS},
   Address = {Fuji Susono, Japan},
   Month = {April},
   Year = {2006}
}

EndNote Reference [help]

Get EndNote Reference (.ref)