Inductive and Coinductive Components of Corecursive Functions in Coq

Yves Bertot 1 Ekaterina Komendantskaya 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for corecursive functions. However, many terminating and productive functions do not pass the syntactic tests. Bove proposed in her thesis an elegant reformulation of the method of accessibility predicates that widens the range of terminative recursive functions formalisable in Constructive Type Theory. In this paper, we pursue the same goal for productive corecursive functions. Notably, our method of formalisation of coinductive definitions of productive functions in Coq requires not only the use of ad-hoc predicates, but also a systematic algorithm that separates the inductive and coinductive parts of functions.
Type de document :
Communication dans un congrès
Jiri Adamek. Coalgebraic Methods in Computer Science, Apr 2008, Budapest, Hungary. 2008
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00277075
Contributeur : Yves Bertot <>
Soumis le : mercredi 9 juillet 2008 - 12:31:12
Dernière modification le : jeudi 11 janvier 2018 - 16:22:54
Document(s) archivé(s) le : mardi 21 septembre 2010 - 16:48:04

Identifiants

  • HAL Id : inria-00277075, version 2
  • ARXIV : 0807.1524

Collections

Citation

Yves Bertot, Ekaterina Komendantskaya. Inductive and Coinductive Components of Corecursive Functions in Coq. Jiri Adamek. Coalgebraic Methods in Computer Science, Apr 2008, Budapest, Hungary. 2008. 〈inria-00277075v2〉

Partager

Métriques

Consultations de la notice

529

Téléchargements de fichiers

393