EECS 598 005: Category Theory for Computer Scientists

Category theory is an area of abstract algebra that studies structures along with their transformations. Categorical structures and universal mapping properties are ubiquitious in mathematics and category theory provides a common language and toolkit that greatly helps to organize mathematical theories.

This course provides an introduction to category theory, focusing on applications relevant to computer science. Specifically we will be focusing on the subfield of categorical logic which applies category theory to the design and analysis of formal logics and programming languages.

There are no formal prerequisites for the course, but it would be helpful to have familiarity with basic notions of programming language theory such as abstract syntax, type systems and formal semantics (operational, axiomatic or denotational). We will cover the relevant notions in an accelerated fashion in the course. Students with mathematical maturity but minimal programming language background are welcome to enroll but should understand 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.

Evaluation

There are four components of your grade:

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

Problem Sets

Problem sets provide challenge problems to ensure mastery of the topics of lecture and the readings. Problem Sets will be posted below in the schedule with their LaTeX source in the github 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. It is always better to submit incomplete or incorrect work than nothing at all.

Students will present solutions to problem sets at the end of certain lecture periods. Signup for a presentation slot on the github.

Final Projects

To complement the material from lecture, students will undertake an independent research project related to category theory. Examples include a survey of an area of category theory not covered in class, implementation of category theory in a proof assistant, or a novel categorical analysis of some area of your own choosing. Students are encouraged to explore an area related to their own research interests.

Scribing

Each lecture will have an assigned scribe who will take notes on the lecture and post a LaTeX copy in the git repo.

Attendance and Participation

In-person attendance in this course is required. If you have a strong interest in taking the course but cannot attend in person, you may discuss your special circumstances with the professor. Lectures will be recorded for reference but this is not a substitute for attendance. Each class will have a sign-in sheet.

Course Schedule and Readings

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

Readings are chosen to complement the lecture. All readings will be from freely available online sources. I recommend reading before attending class. There is no textbook we will directly follow, but the two we will reference the most are Roy Crole’s Categories for Types and Emily Riehl’s Category Theory in Context.

Meeting Date Topic Readings HW Scribe
Mon, Aug 25 Course overview, Intuitionistic Propositional Logic Frank Pfenning notes on natural deduction Shulman Chapter 0 primer on categorical logic Max S. New
Wed, Aug 27 Concrete and Abstract Models of IPL Crole Ch 1.1-1.4
Thu, Aug 28 PS1 Released
Mon, Sep 01 NO CLASS - Labor Day
Wed, Sep 03 Soundness, Completeness, Initiality of Heyting Algebra Semantics
Mon, Sep 08 Simple Type Theory: Syntax and Equational Theory
Wed, Sep 10 Signatures for STT, Set-theoretic Semantics
Thu, Sep 11 PS1 Due, PS2 Released
Mon, Sep 15 Set-theoretic Semantics, Categories
Wed, Sep 17 Categories
Mon, Sep 22 Functors
Wed, Sep 24 Natural Transformations, Universal Properties I (Products)
Thu, Sep 25 PS2 Due, PS3 Released
Mon, Sep 29 Universal Properties II, Exponentials and Presheaves
Wed, Oct 01 Universal Properties III, Representability and Yoneda’s Lemma
Mon, Oct 06 Simple Categories with Families I
Wed, Oct 08 SCwF II
Thu, Oct 09 PS3 Due, PS4 Released
Mon, Oct 13 NO CLASS - Fall Study Break
Wed, Oct 15 SCwF III, Soundness and Completeness
Thu, Oct 16 Final Project Proposals Due
Mon, Oct 20 Logical Relations
Wed, Oct 22 More LR/Natural Numbers Objects
Thu, Oct 23 PS4 Due, PS5 Released
Mon, Oct 27 Inductive Definitions, Structural Recursion
Wed, Oct 29 Equivalence of Categories
Mon, Nov 03 Adjoint Functors
Wed, Nov 05 More Adjoint Functors
Thu, Nov 06 PS5 Due, PS6 Released
Mon, Nov 10 Evaluation Order and Computational Effects
Wed, Nov 12 Monads, Kleisli Categories
Mon, Nov 17 Call-by-value
Wed, Nov 19 Step-indexed models of unbounded Recursion
Wed, Nov 20 PS6 Due
Mon, Nov 24 first-order and higher-order logic, toposes
Mon, Dec 01 dependent type theory
Wed, Dec 03 Final Project Presentations
Mon, Dec 08 Wrap up, Final Project Presentations
Thu, Dec 11 Final Project Writeups Due