Inductive Reasoning for Coinductive Types

Alexander Bagnall, Gordon Stewart, Anindya Banerjee

We present AlgCo (Algebraic Coinductives), a practical framework for inductive reasoning over commonly used coinductive types such as conats, streams, and infinitary trees with fin…