A Functional and Monadic Proof Assistant for Streams

Streams, which are infinite sequences of elements, are defined by a coinductive datatype and operations on streams are corecursive programs. Equations that define streams, under light restrictions, have a unique solution. This project presents the discussion and implementation of a proof assistant...