CoInduction in Coq

Yves Bertot 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We describe the basic notions of co-induction as they are available in the coq system. As an application, we describe arithmetic properties for simple representations of real numbers.
Type de document :
Cours
DEA. EU's coordination action Types Goteborg, 2005
Liste complète des métadonnées

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

https://cel.archives-ouvertes.fr/inria-00001174
Contributeur : Yves Bertot <>
Soumis le : mardi 28 mars 2006 - 17:13:03
Dernière modification le : mercredi 12 septembre 2018 - 01:16:40
Document(s) archivé(s) le : samedi 3 avril 2010 - 21:31:41

Fichiers

Identifiants

Collections

Citation

Yves Bertot. CoInduction in Coq. DEA. EU's coordination action Types Goteborg, 2005. 〈inria-00001174〉

Partager

Métriques

Consultations de la notice

524

Téléchargements de fichiers

317