An introduction to (Co)algebras and (Co)induction and their application to the semantics of programming languages

This report summarizes operational approaches to the formal semantics of programming languages and shows that they can be interpreted inductively by least fixed points as well as coinductively by greatest fixed points. While the inductive interpretation gives semantics to all terminating programs, the coinductive one defines moreover also a semantics for all non-terminating programs. This is especially important in areas where programs do not terminate in general, e.g. data bases, operating systems, or control software in embedded systems. The semantic foundations described in this report can be used to verify that transformations (e.g. in compilers) of such software systems are correct. In the course of this report, coalgebras and coinduction are introduced, starting with a gentle intuitive motivation and ending with a detailed mathematical description within the notions of category theory