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:
- Compile “ofe.v” with “coqc”; this produces a file “ofe.vo”
- Put ofe.vo in a directory in your LoadPath (or add the dir where ofe.vo is to your LoadPath)
- 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.