Author: Yves Bertot
Title: Partial co-recursive functions in the calculus of inductive constructions
Abstract: 
We describe the problems encountered in formalizing filters, which are
typical examples of partial co-recursive on infinite streams.  We propose
a solution and show how this solution can be applied to provide a
new modelization of Eratosthene's sieve.