111 Cummington St., Boston, MA 02215 | cs-www.bu.edu
Last updated: July 20, 2010

Study Group in Category Theory

The study group ran in the Fall 2000. It was aimed at providing a insight into category theory for the working programming languages theory inclined person. We intended on understanding the theory through examples on how category is applied within the field of programming languages.

In the start of the most of the basic definitions were covered. In the fall we will read study examples on how category theory is applied in computer science:

  • The categorical model for the simply typed λ-calculus
  • Monads and the encapsulation of side effects in functional languages.
  • Categorical models for linear logic.

This is the list of the reading that we did. References are given using brackets, e.g.[BW88], and can be found in the bibliography below.

Date Reading
Theory Applications
May 17 [Gold]: Chapter 1, 2, and 3.1-4  
May 24 [Gold]: Chapter 3.5-9  
May 31 [Gold]: Chapter 3.10-14  
June 7 [Gold]: Chapter 3.15-16  
Sep 26   Categorical model for the simply typed λ-calculus. Presented by Elena and Assaf.
Oct 3 Diagrams and natural transformations (4.1-4.3 of [BW88])  
Oct 10
Oct 17
Natural transformations and Yoneda embedding (4.4-4.5 of [BW88])

Sketch of element-style vs. isomorphism styles as presented in [Lev, chp. 10].

Categorical model for the simply typed λ-calculus (7.2 of [Mit])
Oct 24 Adjunctions (3.1 of [Bor])  
Nov 14   Theoretical account of monads (1-2 of [BHM])

Monads and algebras (presented by Paul).

Nov 21   Haskell and monads: type structures and monads (presented by Charles).

Background material can be found in sec 4-5 of [BHM])

Nov 28 Element- and isomorphismstyle (Chp. 10 of [Lev]) Monads and modular denotational semantics

Our meetings were Tuesdays 10-12 am in room B32 (The Church Lab).

Bibliography

[AL]
A. Asperti and G. Longo: Categories, Types, and Structures
[BHM]
Nick Benton,, John Hughes,, and Eugenio Moggi,: Monads and Effects
[Bor]
Francis Borceux: Handbook of Categorical Algebra 1
[BW83]
Michael Barr and Charles Wells: Toposes, Triples and Theories
[BW88]
Michael Barr and Charles Wells: Category theory for computing science
[Gold]
R. Goldblatt: Topoi, The Categorial Analysis of Logic
[Lev]
Paul Blain Levy: Call-By-Push-Value
[Mit]
John C. Mitchell: Foundations for Programming Languages
[Pier]
B. Pierce: Basic Category Theory for Computer Scientists

Participants