Constructing Programs with Bird-Meertens Formalism

Abstrakt:

In this seminar we present Bird Meertens formalism, a mathematical tool for the construction of generic (datatype-parametric) programs. We define the formalism starting from the category FUN of sets and total functions, and explain how recursive datatypes are represented by fixpoints of functors. We define catamorphism and anamorphism as fundamental building blocks in the formalism, and then turn to concrete examples of program derivation. We conclude by describing our current research in the area.