An introduction to Initial Algebra Semantics

Kobe Wullaert

Inductive data types have become an important tool in functional programming and in particular in the design of programming languages as they are used to define the type of terms in the sought language. Initial Algebra Semantics characterizes the set of terms, using the framework of Category Theory, as initial objects in specific categories, those of F-algebras. In this talk, we first introduce the necessairy background of Category Theory. Then, we work our way up to the general framework of F-algebras guided by examples.

---

Previous: | Computer formalization of Voevodsky's theory of type theories
Next: | Function Inlining as a Language Parametric Refactoring