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 that supports this proof method. The tool is implemented in the purely functional language Haskell and makes extensive use of monads. The emphasis of the project is placed on simplicity, clarity and terseness.