|||Sabine Glesner, An Introduction to (Co)Algebras and
(Co)Induction and their Application to the Semantics of Programming Languages, Nr. 2005-22, August 2005.
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.