Syntax, Types, Equations | CfT 3.1-3 | Sep 01 | Algebraic Type Theory

Categorical Semantics and Soundness | CfT 3.4-6 | Due: A01

Out: A02 Sep 06 | Algebraic Type Theory

Categories of Models | CfT 3.7 | Sep 08 | Algebraic Type Theory

Classifying Category | CfT 3.7-8 | Due: A02

Out: A03 Sep 13 | Algebraic Type Theory

Classifying Category | CfT 3.8-9 | Sep 15 | CT: Representable Functors | BCT 4, CT 8.3-4 | Due: A03

Out: A04 Sep 20 | CT: Cartesian Closed Categories

Functional Type Theory: Syntax | CfT 2.8, 4.1-3, CT 6 | Sep 22 | Functional Type Theory

Categorical Semantics and Soundness | CfT 4.4-6 | Due: A04

Out: A05 Sep 27 | Functional Type Theory

Classifying Category | CfT 4.7-9 | Sep 29 | Functional Type Theory

Categorical Gluing | CfT 4.10 | Due: A05 Oct 04 | Functional Type Theory

Proving Conservativity | CfT 4.10 | Oct 06 | CT: Adjoint Functors | BCT 2, CT 9.1-5 | Out: A06 Oct 11 | **FALL BREAK: NO CLASS** | **NO CLASS** | **NO CLASS** Oct 13 | Polymorphic Type Theory

Syntax, Types, Equations | CfT 5.1-2, PFPL 16 | Oct 18 | Polymorphic Type Theory

Categorical Semantics:

Types and terms in type context | CfT 5.3-4 | Oct 20 | Polymorphic Type Theory

Categorical Semantics:

Type and term substitutions | CfT 5.3-5.4 | Due: A06

Out: A07 Oct 25 | Polymorphic Type Theory

Categorical Semantics:

Polymorphic types and terms | CfT 5.3-5.4 | Oct 27 | CT: Limits and Colimits | BCT 5, CT 5.4-6 | Nov 01 | CT: Algebras and Coalgebras

Inductive Types | [#Métayer] | Nov 03 | Initial Algebras

Fixed-Points of Functors | [#Métayer] | Due: A07

Out: A08 Nov 08 | Continuous Functors

Domain Equations | [#Métayer]

[#SP] and [#AMM] | Nov 10 | CT: Monoidal Categories

Linear Logic: Multiplicatives | [#Benton] | Nov 15 | CT: Comonads

Linear Logic: Exponentials | CT 10.4

[#Benton] | Nov 17 | Linear logic: LNL models

CT: Monads, Effects, Kleisli Triples | [#Benton]

[#Moggi] | Due: A08

Out: A09 Nov 22 | CT: More Monads, Kleisli Category

Monadic Metalanguage | CT 10.1-2

[#Moggi] | Nov 24 | **THANKSGIVING: NO CLASS** | **NO CLASS** | **NO CLASS** Nov 29 | CT: Monads and Algebras

Algebraic Effects | CT 10.3

[#Bauer] | Dec 01 | Algebraic Effects | [#Bauer] | Due: A09 **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 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.