[Back to Teaching]
Category theory is an abstract mathematical language that is used in many different branches of mathematics. It has also found its successful applications in computer science---in fact, in many different ways. The classic example is in the semantics of functional programming, where types are objects and programs are arrows. In this course we focus on another eminent use of categories in computer science, namely categorical algebra and coalgebra.
The bottom-line here is: a coalgebra is a categorical abstraction of dynamics, i.e. a state-based system like an automaton; and an algebra (especially an initial one) is an abstraction of syntax, i.e. the set of well-formed programs. Plotkin's structural operational semantics---connecting syntax and dynamics—also allows an elegant categorical modeling via a distributive law.
After exhibiting these basics of the (co)algebraic modeling in computer science, we proceed to a more advanced categorical structure of presheaf categories. We introduce the necessary categorical machineries—(co)end, Kan extension, the Yoneda lemma, etc.—as well as demonstrate their applications in name-passing calculi like pi-calculus.
No preliminary knowledge in category theory is assumed. The course materials will be announced at the course website.
Keywords: Theoretical computer science; category theory; algebra; coalgebra; automaton; semantics of programming language; presheaf
Rough notes to be revised soon. The revised notes will be available
here.
Part 1
Part 2
Part 3
Part 4
Based on a report. (due at 16.59, Wed 8 August 2012)