J’ai développé un outil aidant à la définition et au raisonnement sur les fonctions récursives générales dans Coq [BFPR06].

Cet outil a été intégré à Coq à partir de la version 8.1 sous le mot clef Function. Il permet de définir aisément des fonctions récursives dont la terminaison ne repose plus simplement sur la décroissance structurelle d’un argument mais sur l’accessibilite de cet argument. Afin de faciliter le raisonnement, une équation de point fixe et un principe d’induction spécifique à la fonction sont également automatiquement générés.

• Publications

This document was translated from L^AT_EX by H^EV^EA.