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

give axiomatic and denotational semantics to different kinds of logics and programming languages
carry out basic 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 (70%)
In-class presentation of solutions (10%): we will set aside class time to review the solutions to problem sets
Scribing (10%): students will contribute notes written in LaTeX of the in-class lectures to share with the entire class.
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.

Scribing

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.

Attendance

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	PS1 Due, PS2 Released	Yanjun Chen
Wed, Jan 25	Signatures for STT, Set-theoretic Semantics	Crole Ch 3
Mon, Jan 30	Categories, Functors
Wed, Feb 01	Universal Mapping Properties and Yoneda’s Lemma		PS2 Due, PS3 Released
Mon, Feb 06	Initiality of STT in Cartesian Closed Categories
Wed, Feb 08	Disjunction Property for STT
Mon, Feb 13	Inductive Datatypes, Axiomatics		PS3 Due, PS4 Released
Wed, Feb 15	Inductive Datatypes, Models
Mon, Feb 20	Evaluation Order and Computational Effects
Wed, Feb 22	Concrete Models of Effects, Adjoint Functors		PS4 Due
Mon, Feb 27	NO CLASS - SPRING BREAK
Wed, Mar 01	NO CLASS - SPRING BREAK
Mon, Mar 06	Monads and Algebras		PS5 Released
Wed, Mar 08	Call-by-push-value
Mon, Mar 13	Recursive programs and datatypes, fixed points
Wed, Mar 15	Basic Domain Theory		PS5 Due, PS6 Released
Mon, Mar 20	Solving Domain Equations
Wed, Mar 22	Guarded Domain Theory
Mon, Mar 27	Intuitionistic Linear Logic, Monoidal Categories		PS6 Due, PS7 Released
Wed, Mar 29	Models of ILL
Mon, Apr 03	Bunched Implications/Separation Logic
Wed, Apr 05	Dependent Type Theory		Ps7 Due, PS8 Released
Mon, Apr 10	Fibrations, Categories with Families
Wed, Apr 12	Presheaf Models		PS8 Due
Mon, Apr 17	Subobject Classifiers, Toposes

EECS 598 005: Category Theory for Computer Scientists