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.
Document type :
Lectures
Liste complète des métadonnées

Cited literature [19 references]  Display  Hide  Download

https://cel.archives-ouvertes.fr/inria-00001174
Contributor : Yves Bertot <>
Submitted on : Tuesday, March 28, 2006 - 5:13:03 PM
Last modification on : Wednesday, September 12, 2018 - 1:16:40 AM
Document(s) archivé(s) le : Saturday, April 3, 2010 - 9:31:41 PM

Files

Identifiers

Collections

Citation

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

Share

Metrics

Record views

641

Files downloads

335