A Functional and Monadic Proof Assistant for Streams

Abstract

Streams, which are infinite sequences of elements, are defined by a coinductive datatype and operations on streams are corecursive pro­grams. Equations that define streams, under light restrictions, have a unique solution. This project presents the discussion and imple­mentation 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 pla­ced on simplicity, clarity and terseness.