CoInduction in Coq

Yves Bertot (1)

1 MARELLE - Mathematical, Reasoning and Software

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.

Mots clés: Calculus of inductive constructions; Coq; Co-induction

Domaines: Logique en informatique [cs.LO]

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