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 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.
Type de document :
Communication dans un congrès
Functional and Logic Programming (FLOPS'06), 2006, Fuji Susono, Japan. 2006
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00564237
Contributeur : Mister Dart <>
Soumis le : mardi 8 février 2011 - 15:26:06
Dernière modification le : jeudi 11 janvier 2018 - 16:22:53
Document(s) archivé(s) le : lundi 9 mai 2011 - 03:09:46

Fichier

2006-FLOPS.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00564237, version 1

Collections

Citation

Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu. Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. Functional and Logic Programming (FLOPS'06), 2006, Fuji Susono, Japan. 2006. 〈inria-00564237〉

Partager

Métriques

Consultations de la notice

200

Téléchargements de fichiers

143