Categories, Proofs and Programs

Synopsis

• Introduction to category theory. Categories, functors, natural transformations. Isomorphisms. monics and epics. Products and coproducts. Universal constructions. Cartesian closed categories. Symmetric monoidal closed categories. The ideas will be illustrated with many examples, from both mathematics and Computer Science.
• Introduction to structural proof theory. Natural deduction, simply typed lambda calculus, the Curry-Howard correspondence. Introduction to Linear Logic. The connection between logic and categories.
• Further topics in category theory. Algebras, coalgebras and monads. Connections to programming (structural recursion and corecursion), and to programming languages (monads as types for computational effects).