Daniel Freiermuth: Bachelor's Thesis

Saarland University Computer Science

Formalizing stream calculus using coinduction

Advisors: Steven Schäfer


We formalize the principle of stream calculus in coq. Employing coinduction we will define several structures on those, especially streams as generating functions and expontial generating functions. Using those structures we will be able derive and proof the explicit forumula of Fibonacci and show some other basic results.


Daniel Freiermuth, Mon Mar 5 15:29:39 2018