EECS 598 005: Category Theory for Computer Scientists

Category theory is a mathematical theory of structures and transformations. While originally developed for applications to pure mathematics, category theory has become a useful tool for studying logic and programming languages.

The breadth of applications and high level of abstraction can make category theory difficult to approach for those without an extensive math background. This course aims to introduce and motivate category theory by focusing on applications in computer science, in particular to logic and programming languages.

Students are expected to have familiarity with basic notions of programming language theory such as abstract syntax, type systems and some form of formal semantics (operational, axiomatic or denotational). Students with a strong math background but minimal programming language background are also welcome to enroll but the focus of the class will be on these computer science applications.

Learning Objectives

After completing this course, students should be able to

Degree Requirements

To see what degree requirements this course satisfies, see the spreadsheet on this page.


There are four components of your grade:

  1. Problem Sets (70%)
  2. In-class presentation of solutions (10%): we will set aside class time to review the solutions to problem sets
  3. Scribing (10%): students will contribute notes written in LaTeX of the in-class lectures to share with the entire class.
  4. Participation (10%): attendance and participation in lecture.

Problem Sets

Problem Sets will be posted below in the schedule with their LaTeX source in the gitlab repo. You can complete them in groups of 2 or 3. You will submit them on Canvas as a pdf. You may include hand-drawn diagrams, but text and equations should be typeset in LaTeX.

Problem sets will be always be due at 11:59pm on the listed due date. Late work will not be accepted.

Students will present solutions to problem sets at the end of certain lecture periods. Signup for this on the gitlab repo.


This semester will use a new curriculum without following a single textbook. To help everyone in the class, each lecture will have an assigned scribe who will take notes on the lecture and post a LaTeX copy in the gitlab repo.


Participating in this course means attending lecture in person. Lectures will be recorded but this is not a substitute for attendance. Each class will have a sign-in sheet.

Course Schedule

The following schedule of topics and homeworks is tentative and will be updated throughout the semester.

We will have two weeks of no lecture during the semester: the week of MLK day and spring break. There will not be a homework due after spring break but there will be after MLK week (since only one day is an academic holiday).

Readings are chosen to complement the lecture. All readings will be from freely available online sources.

Meeting Date Topic Readings HW Scribe
Wed, Jan 04 Course overview, Propositional Logic Frank Pfenning notes Max S. New
Mon, Jan 09 Models of Propositional Logic Crole Ch 1.1-1.4 PS1 Released Alan Yang
Wed, Jan 11 Soundness, Completeness, Initiality of Heyting Algebra Semantics Zhemin Qu
Mon, Jan 16 NO CLASS - MLK Day
Wed, Jan 18 NO CLASS - POPL
Mon, Jan 23 Simple Type Theory: Syntax and Axiomatic Semantics Crole Ch 4.1-4.3, STT Full Rules PS1 Due, PS2 Released Yanjun Chen
Wed, Jan 25 Signatures for STT, Set-theoretic Semantics Crole Ch 3 Chris Jiang
Mon, Jan 30 Set-theoretic Semantics, Categories Crole Ch 2.1-2.2 Jonah Nan
Wed, Feb 01 Categories Riehl Ch 1.1-1.2 Han Jiang
Fri, Feb 03 PS2 Due, PS3 Released
Mon, Feb 06 Functors Crole Ch 2.3, Riehl Ch 1.3 Wen Plotnick
Wed, Feb 08 Natural Transformations, Universal Properties I (Products) Crole Ch 2.4,2.6,2.8, Riehl Ch 1.4 Steven Schaefer
Mon, Feb 13 Universal Properties II, Exponentials and Predicators Riehl Ch. 2.1 PS3 Due, PS4 Released Runze Xue
Wed, Feb 15 Universal Properties III, Representability and Yoneda’s Lemma Riehl Ch. 2.2-2.3 Shubh Agrawal
Mon, Feb 20 C-T Structures I Riehl Ch. 2.3-2.4 Jigang Li
Wed, Feb 22 C-T Structures II Crole Ch. 4.5-4.9 Yuchen Jiang
Fri, Feb 05 PS4 Due
Mon, Mar 06 C-T Structures III, Soundness and Completeness Crole Ch. 4.5-4.9 PS5 Released Jin Pan
Wed, Mar 08 Logical Relations Crole Ch. 4.10 Benjamin Kelly
Mon, Mar 13 More LR/Natural Numbers Objects Hutton JFP ’99 Pranav Srinivasan
Wed, Mar 15 Inductive Datatypes McBride POPL ’08 Kevin Wang
Mon, Mar 20 Evaluation Order and Computational Effects Levy Chapter 1 PS5 Due, PS6 Released Michael Xi
Wed, Mar 22 Equivalence of Categories Riehl Ch 1.5 Daiwen Zhang
Mon, Mar 27 Adjoint Functors Riehl Ch 4.1-4.3 Jonathan Moore
Wed, Mar 29 More Adjoint Functors Levy Chapter 2 Owen Goebel
Fri, Mar 31 PS6 Due, PS7 Released
Mon, Apr 03 Call-by-push-value Eric Zhao
Wed, Apr 05 Call-by-push-value II Elanor Tang
Mon, Apr 10 Effects in CBPV PS7 Due, PS8 Released
Wed, Apr 12 Models of CBPV Matt Wang
Mon, Apr 17 Review and Conclusions Darren Fitzgerald
Fri, Apr 21 PS8 Due Matthew Nomura