CSE 598 005: Category Theory for Computer Scientists
- Lecture: Monday & Wednesday, 2:30-4:30pm, Beyster 1620
- Instructor: Max S. New
- Office: Beyster 4628
- uniqname: maxsnew
- Office Hours: Tuesdays and Thursdays 3:30-5pm or by appointment
- Canvas
- Lecture capture
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
- give axiomatic and denotational semantics to different kinds of logics and programming languages
- carry out proofs in order theory and category theory
- learn and explore further applications of order theory and category theory on their own, especially in programming language research papers
Degree Requirements
To see what degree requirements this course satisfies, see the spreadsheet on this page.
Evaluation
There are four components of your grade:
- Problem Sets (60%)
- Final Project (20%)
- In-class presentation of solutions (10%): we will set aside class time to review the solutions to problem sets
- Scribing (5%): students will contribute notes written in LaTeX of the in-class lectures to share with the entire class.
- 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 | Ivan Wei | |
| Thu, Aug 28 | PS1 Released | |||
| Mon, Sep 01 | NO CLASS - Labor Day | |||
| Wed, Sep 03 | Soundness, Completeness, Initiality of Heyting Algebra Semantics | Ayan Chowdhury | ||
| Mon, Sep 08 | Simple Type Theory: Syntax and Equational Theory | Crole Ch 4.1-4.3 | Alexander Bandukwala | |
| Wed, Sep 10 | Set-theoretic Semantics, Categories | Crole Ch 3 | Jesse Slater | |
| Thu, Sep 11 | PS1 Due, PS2 Released | |||
| Mon, Sep 15 | PS1 Review, Categories | Crole Ch 2.1-2.2, Riehl Ch 1.1-1.2 | Chris Davis | |
| Wed, Sep 17 | Functors, Natural Transformations | Crole Ch 2.3,2.4,2.6,2.8, Riehl Ch 1.3-1.5 | Yuchen Jiang | |
| Mon, Sep 22 | Equivalence of Categories | Riehl Ch 1.6 | Yichen Tiao | |
| Wed, Sep 24 | Universal Properties, Presheaves | Riehl Ch 2 | Eric Bond | |
| Thu, Sep 25 | PS2 Due, PS3 Released | |||
| Mon, Sep 29 | PS2 Review, Universal Properties II | Riehl Ch 2 | ||
| Wed, Oct 01 | Universal Propertie | Riehl Ch 2 | Yuchen Jiang | |
| Mon, Oct 06 | biCCC, Simple Categories with Families, Initiality of STLC | Crole Ch. 4.5-4.9 | Conner Rose | |
| Wed, Oct 08 | Initiality of STLC | Crole Ch. 4.10 | Eric Bond | |
| Thu, Oct 09 | PS3 Due, PS4 Released | |||
| Mon, Oct 13 | NO CLASS - Fall Study Break | |||
| Wed, Oct 15 | Steven Schaefer Guest Lecture: Initiality of STLC II | |||
| Thu, Oct 16 | Final Project Proposals Due | |||
| Mon, Oct 20 | PS3 Review, Canonicity of STLC | |||
| Wed, Oct 22 | Canonicity II | Alexander Bandukwala | ||
| Mon, Oct 27 | PS4 Review, Natural Numbers Objects, Inductive Types | Hutton JFP ’99 | ||
| Wed, Oct 29 | Initial Algebras and Terminal Coalgebras | Adamek-Milius-Moss Ch 1 | ||
| Thu, Oct 30 | PS4 Due, PS5 Released | |||
| Mon, Nov 03 | Evaluation Order and Computational Effects | Levy Chapter 1 Moggi 89 | ||
| Wed, Nov 05 | PS4 Review, Strong Monads and Kleisli Categories | Moggi 91 | ||
| Mon, Nov 10 | Algebra, Adjoint Functors | Bauer 2018 | Ayan Chowdhury | |
| Wed, Nov 12 | Adjunctions | Riehl Ch 4.1-4.3 | Chris Davis | |
| Thu, Nov 03 | PS5 Due, PS6 Released | |||
| Mon, Nov 17 | Call-by-push-value I | Levy Chapter 2 | ||
| Wed, Nov 19 | Call-by-push-value II | Conner Rose | ||
| Mon, Nov 24 | Domain Theory I: Traced Cartesian Categories, DCPOs | Conner Rose | ||
| Tue, Nov 25 | PS6 Due | |||
| Mon, Dec 01 | PS5 Review, Domain Theory II: Recursive functions, Kleene’s Fixed Point theorem | |||
| Wed, Dec 03 | Constructing Inductive Types | Adamek-Milius-Moss Ch 2 | ||
| Mon, Dec 08 | Final Project Presentations | |||
| Thu, Dec 11 | Final Project Writeups Due |