[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
教科書：
印刷用 (4up)：
希望者には講義の初回に印刷したものを配布する．
その他参考書は，
レポートによる．教育研究支援室横レポート提出ボックスか，または講師のメールアドレス宛提出すること．締切は 2013/8/9 (FRI) 23:59 (JST).