Advisors: Steven SchÃ¤fer
Sequences of elements of type T are common in discrete mathematics and computer science. Stream-Caculus is a powerful and clean tool for dealing with those, capable even of handling more involved ones (like non-trivial recurrence relations) and not only useful for proving propositions, but even deriving them. Having a ring structure on T, we can lift that to a ring structure on the Streams on T and use that to reason on the level of Streams. This is highly motivated by ordinary and exponential generating functions. As Streams are coinductive we need some tweaks in order to formalize Streams and operations thereon in Coq.