**Cornell CS 6117: Category Theory for Computer Scientists (Fall 2025)** (#) Announcements - 08/25: Welcome to CS 6117! # Syllabus Category theory is an abstract theory of structures and transformations. While originally motivated by pure mathematics, category theory has since found applications across physics, philosophy, linguistics, logic, and more; the area is under active development and continues to evolve. The breadth of applications and high level of abstraction can make category theory difficult to approach. This course aims to introduce and motivate category theory by focusing on applications in computer science, and in particular programming language semantics. (##) Course Information This is a graduate-level course. Undergraduates are welcome to enroll with permission of the instructor. The main pre-requisite for this course is CS 6110 or CS 4110. Although this course is offered in the computer science department, it is a **purely theoretical course**. There will be no programming involved, and students will be **required to do proofs for all homework assignments**. (##) Course Objectives After completing this course, students should be able to (a) give categorical semantics to different kinds of programming languages and programming language features, (b) carry out basic proofs in category theory, (c) learn and explore further applications of category theory on their own, building on their familiarity with basic concepts and methods in category theory, and (d) explain the basic concepts of a variety of denotational semantics. (##) Logistics - Lectures: Hollister 366, Tuesdays and Thursdays 1:25 PM - 2:40 PM - Questions: [Edstem](https://edstem.org/us/join/9beXXM) (##) Staff Instructor: Justin Hsu - Web: - Email: - Office hours: Wednesday 2:30-3:30 in Gates 446 (##) Assessment Course grades will be based entirely on homework assignments. There are no exams. (###) Assignments There will be one assignment every other week. Submissions must be typeset in LaTeX (you can use [quiver](https://q.uiver.app/) for commutative diagrams). - Assignments are due **Thursdays anytime before class**. - Late assignments are not accepted. - Your lowest assignment will not be counted. - Assignments will be posted and submitted on [CMS](https://cmsx.cs.cornell.edu). (###) Gold-Star Grading We will be using the simplified grading scheme from CS 6110. Our goal is to focus on giving you useful feedback, not on precisely scoring every granular facet of a homework problem. There are three possible outcomes: - **Gold star**: If you do everything reasonably well, whether you have lots of mistakes or are more or less perfect, you will receive a gold star. Congratulations! - **Sparkly star**: If you do something surprisingly awesome, you will receive a *sparkly* star. (This is uncommon.) - **No star**: If your work has major gaps or significant misunderstanding, you may receive no stars. (This is also uncommon.) As a rough guide, earning gold stars on every counted assignment will achieve an A in your course grade. If you are taking this course S/U, earning a gold star on at least four (4) assignments will achieve an S. # Resources For the first half of the course, we will follow **Categories for Types (CfT)** by Roy Crole. Cornell students should have access to the electronic version available [here](https://www.cambridge.org/core/books/categories-for-types/258841251C62FED1DACD20884E59E61C). For the second half of the course, we will follow selected research papers---see the schedule below. While CfT is self contained, the introduction of category theory material is terse. There are many good presentations and resources focused on just category theory. We suggest: - **Basic Category Theory (BCT)** by Tom Leinster. A good introduction to the basics. [Electronic version](https://arxiv.org/abs/1612.09375). - **Category Theory (CT)** by Steve Awodey. Another good textbook. [Electronic version](https://academic-oup-com.proxy.library.cornell.edu/book/7134). - **Category Theory in Context (CTiC)** by Emily Riehl. More comprehensive, with many examples from mathematics. [Electronic version](https://math.jhu.edu/~eriehl/context.pdf). - **nLab**. A curated wiki for category theory and related topics. Extremely useful as a reference, but (a) it can be a bit hard to navigate/discover pages, and (b) articles use a terse and abstract style that takes some getting used to. [nlab](https://ncatlab.org). CfT (and our course) illustrate category theory through applications to programming language semantics. We will assume a working knowledge of the basics (e.g., as covered in CS 6110), and we will introduce more as we go. Here are some good references for PL semantics: - **Categorical Logic and Type Theory (CLaTT)** by Bart Jacobs. In the same vein as CfT, but goes much deeper and covers many more advanced topics. A bible, most useful as a reference. - **Practical Foundations for Programming Languages** by Robert Harper. [Draft version](http://www.cs.cmu.edu/~rwh/pfpl/). - **Types and Programming Languages** by Benjamin C. Pierce. [Website](https://www.cis.upenn.edu/~bcpierce/tapl/). - **PLS Lab**. Wiki on Programming, Logic and Semantics, with a focus on concise definitions, examples, and references. [pls-lab](https://www.pls-lab.org/). - **Stanford Encyclopedia of Philosophy**. High-quality, peer-reviewed articles. Most useful for articles on logic, but also some overlap with PL. [sep](https://plato.stanford.edu/). # Schedule All dates and topics are tentative and subject to change. Lecture | Date | Topic | Readings | Assignments :------:|:------:|-------|----------|:-----------: 01 | Aug 26 | CT: Basics | CfT 2.1-4 | 02 | Aug 28 | CT: Basics | CfT 2.5-6 | Out: A1 03 | Sep 02 | Algebraic Type Theory:
Syntax, Types, Equations | CfT 3.1-3 | 04 | Sep 04 | Algebraic Type Theory:
Semantics and Soundness | CfT 3.4-6 | 05 | Sep 09 | Algebraic Type Theory:
Categories of Models | CfT 3.7 | 06 | Sep 11 | Algebraic Type Theory:
Classifying Category | CfT 3.8-9 | Due: A1
Out: A2 07 | Sep 16 | CT: Representable Functors | BCT 4, CT 8.3-4 | 08 | Sep 18 | CT: Cartesian Closed Categories
Functional Type Theory: Syntax | CfT 2.8, 4.1-3, CT 6 | 09 | Sep 23 | Functional Type Theory: Semantics and Soundness | CfT 4.4-6 | 10 | Sep 25 | Functional Type Theory: Classifying Category | CfT 4.7-9 | Due: A2
Out: A3 11 | Sep 30 | Functional Type Theory: Categorical Gluing | CfT 4.10 | 12 | Oct 02 | Functional Type Theory: Conservativity | CfT 4.10 | 13 | Oct 07 | CT: Adjoint Functors | BCT 2, CT 9.1-5 | 14 | Oct 09 | Sized Type Theory:
Syntax, Types, Equations | CfT 5.1-2, PFPL 16 | Due: A3
Out: A4 -- | Oct 14 | **FALL BREAK** | -- | -- 15 | Oct 16 | Sized Type Theory:
Indexed Semantics:
Types, Terms, Substitutions | CfT 5.3-4 | 16 | Oct 21 | Sized Type Theory:
Indexed Semantics:
Size Polymorphism | CfT 5.3-4 | 17 | Oct 23 | CT: Fibered Categories | | Due: A4
Out: A5 18 | Oct 28 | Sized Type Theory:
Fibered Semantics | | 19 | Oct 30 | CT: Limits and Colimits | BCT 5, CT 5.4-6 | 20 | Nov 04 | CT: Algebras and Coalgebras
Inductive Types | [#Métayer] | 21 | Nov 06 | Initial Algebras
Fixed-Points of Functors | [#Métayer] | Due: A5
Out: A6 22 | Nov 11 | Continuous Functors
Domain Equations | [#Métayer]
[#SP] and [#AMM] | 23 | Nov 13 | CT: Monoidal Categories
Linear Logic: Multiplicatives | [#Benton] | 24 | Nov 18 | CT: Comonads
Linear Logic: Exponentials | [#Benton] | 25 | Nov 20 | Linear logic: LNL models
CT: Monads and Effects | [#Benton]
[#Moggi] | Due: A6
Out: A7 26 | Nov 25 | CT: More Monads
Monadic Metalanguage | CT 10.1-2
[#Moggi] | -- | Nov 27 | **THANKSGIVING BREAK** | -- | -- 27 | Dec 02 | CT: Monads and Algebras
Algebraic Effects | CT 10.3
[#Bauer] | 28 | Dec 04 | Algebraic Effects | [#Bauer] | Due: A7
Out: A8 -- | Final (TBD) | -- | -- | Due: A8 **Readings**: [#Métayer]: François Métayer. Fixed points of functors. 2003. [[pdf](https://www.irif.fr/~metayer/PDF/fix.pdf)] [#SP]: Michael B. Smyth and Gordon D. Plotkin. The Category-Theoretic Solution of Recursive Domain Equations. 1982. [[pdf](https://homepages.inf.ed.ac.uk/gdp/publications/Category_Theoretic_Solution.pdf)] [#AMM]: Jiří Adámek, Stefan Milius, Lawrence S. Moss. Fixed Points of Functors. 2016. [[pdf](https://www.sciencedirect.com/science/article/pii/S2352220816301201)] [#Benton]: P. N. Benton. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract). 1995. [[pdf](http://nickbenton.name/cslpaper.pdf)] [#Moggi]: Eugenio Moggi. Notions of Computation and Monads. 1991. [[pdf](https://www.sciencedirect.com/science/article/pii/0890540191900524)] [#Bauer]: Andrej Bauer. What Is Algebraic about Algebraic Effects and Handlers? 2019. [[pdf](https://arxiv.org/pdf/1807.05923.pdf)] # Policies (##) Academic Integrity Cornell University has a Code of Academic Integrity (see [here](https://theuniversityfaculty.cornell.edu/dean/academic-integrity/)). Violations of this code are treated very seriously by Cornell and can have long-term repercussions. In this course, you are encouraged to discuss the content of the course with other students, and you may also discuss homework problems with other students. However: - You must do your own work and write up assignments individually, without shared notes of any kind. - If you discuss a problem with another student, you are expected to document this fact in your write-up. - Unless otherwise stated, you may freely use any of the resources above. However, searching for or copying solutions from other sources---including any form of generative AI---is not allowed. (##) Respect in Class Everyone—the instructor, TAs, and students—must be respectful of everyone else in this class. All communication, in class and online, will be held to a high standard for inclusiveness: it may never target individuals or groups for harassment, and it may not exclude specific groups. That includes everything from outright animosity to the subtle ways we phrase things and even our timing. For example: do not talk over other people; don't use male pronouns when you mean to refer to people of all genders; avoid explicit language that has a chance of seeming inappropriate to other people; and don't let strong emotions get in the way of calm, scientific communication. If any of the communication in this class doesn't meet these standards, please don't escalate it by responding in kind. Instead, contact the instructor as early as possible. If you don't feel comfortable discussing something directly with the instructor—for example, if the instructor is the problem—please contact the advising office or the department chair. (##) Special Needs and Wellness It is Cornell policy to provide reasonable accommodations to students who have a documented disability (e.g., physical, learning, psychiatric, vision, hearing, or systemic) that may affect their ability to participate in course activities or to meet course requirements. Students with disabilities are encouraged to contact [Student Disability Services](http://sds.cornell.edu/) at 607-254-4545, or the instructor for a confidential discussion of their individual needs. If you are experiencing undue personal or academic stress at any time during the semester or need to talk to someone who can help, contact the instructor or: - [Engineering Academic Advising](https://www.engineering.cornell.edu/resources/advising/) at 607-255-7414, - [Learning Strategies Center](http://lsc.cornell.edu/) at 607-255-6310, - [Let's Talk Drop-in Counseling](https://health.cornell.edu/services/counseling-psychiatry/lets-talk) at Gannett at 607-255-5155 - [Empathy Assistance and Referral Service](http://orgsync.rso.cornell.edu/org/ears) at 607-255-EARS.