The Coq formalization described in the paper

Pietro Di Gianantonio, Marino Miculan, A Unifying Approach to Recursive and Co-recursive Definitions. In Geuvers, Wiedijk, editors, Proceedings of TYPES’02. LNCS 2646, 2003.

is available in this zip file, where you can find:

• “ofe.v”: basic definitions, theorems about existence of fixed points
• “primes.v”: example application: definition of the (real) stream of prime numbers (the Sieve)
• (The original development, as per the published paper, for Coq version 7.3)

How to use:

1. Compile “ofe.v” with “coqc”; this produces a file “ofe.vo”
2. Put ofe.vo in a directory in your LoadPath (or add the dir where ofe.vo is to your LoadPath)
3. Import “ofe” within coqc or coqtop, using “Require ofe”. See primes.v for an example.

Please drop us a note if these libs are useful to you.