  We present AlgCo (Algebraic Coinductives), a practical framework for
inductive reasoning over commonly used coinductive types such as conats,
streams, and infinitary trees with finite branching factor. The key idea is to
exploit the notion of algebraic complete partial order from domain theory to
define continuous operations over coinductive types via primitive recursion on
``dense'' collections of their elements, enabling a convenient strategy for
reasoning about algebraic coinductives by straightforward proofs by induction.
We implement the AlgCo framework in Coq and demonstrate its power by verifying
a stream variant of the sieve of Eratosthenes, a regular expression library
based on coinductive trie encodings of formal languages, and expected value
semantics for coinductive sampling processes over discrete probability
distributions in the random bit model.
