KIT | KIT-Bibliothek | Impressum
Open Access Logo
URN: urn:nbn:de:swb:90-41216

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

Glesner, Sabine


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.

Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Forschungsbericht
Jahr 2005
Sprache Englisch
Identifikator ISSN: 1432-7864
KITopen ID: 1000004121
Verlag Karlsruhe
Serie Interner Bericht. Fakultät für Informatik, Universität Karlsruhe ; 2005,22
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page