CS 6118 (Fall 2012)  Types and Semantics
Overview
CS6118  Types and Semantics is about designing and understand programming languages, whether they be domain specific or general purpose. The goal of this class is to provide a variety of tools for designing custom (programming) languages for whatever task is at hand. Part of that will be a variety of insights on how languages work along with experiences from working with academics and industry on creating new languages such as Ceylon and Kotlin. The class focuses on types and semantics and the interplay between them. This means category theory and constructive type theory (e.g. Coq and richer variations) are ancillary topics of the class. The class also covers unconventional semantic domains such as classical linear type theory in order to both break students from convential thinking and to provide powerful targets capable of formalizing thinks like networking protocols, resourcesensitive computation, and concurrency constructs. The class project is to design and formalize a (programming) language for a purpose of the student's choosing, and assignments are designed to ensure students have had a chance to practice applying the techniques learned in class before culminating these skills in the class project.
Class Times: TuTh 2:554:10
Location: Snee Hall 1120
Instructor:
Ross Tate
Office: 4136 Upson Hall
Office Hours: Wed. 1:002:00 and by appointment
Grading There will be seven homework assignments, a project, a midterm, and a (noncummulative) final. The breakdown is:
Assignments: 35%
Project: 25%
Midterm: 20%
Final: 20%
Related Reading
 Abstract and Concrete Categories  The Joy of Cats by Jiri Adamek, Horst Herrlich, and George E. Strecker (2004)
 Using Category Theory to Design Implicit Conversions and Generic Operators by John C. Reynolds (1980)
Schedule
Date  Topic  Notes  Assignments 

Week 1  
Aug 23  Goals of the Course Discussion of Student Interests Overview of Language Design Challenges 
(none)  
Week 2  
Aug 28  Semantics of Subtyping Basic Category Theory: Categories and Functors 
Lecture 2  
Aug 30  WAT Naturality of Operators Static/Dynamic Behavorial Subtyping Principal Types 
Lecture 3  
Week 3  
Sep 4  Introduction to Coq Inductive Data Types Dependent Matches 
Lecture 4 Coq Code 

Sep 6  Equality in Coq Formalizing Subtyping in Coq 
Lecture 5 Coq Code Homework Code 

Week 4  
Sep 11  Lists and Comprehensions  Lecture 6  
Sep 13  SQL and Opfibrations  Lecture 7  Homework 1 Due 
Week 5  
Sep 18  Opfibrations in Detail  Lecture 8 Opfibration Notes 

Sep 20  SQL Joins: Products in Opfibrations  Lecture 9  
Week 6  
Sep 25  Aggregation: Monad Algebras  Lecture 10  
Sep 27  Lifting Expressions: Monoidal Functors  Lecture 11  Homework 2 Due 
Week 7  
Oct 2  Midterm Review  Lecture 12  Bring Questions!!! 
Oct 4  Midterm  
Week 8  
Oct 9  No Class Celebrate Canadian Thanksgiving! 

Oct 11  Intuitionist Logic CurryHoward Isomorphism 
System PJ  
Week 9  
Oct 16  Classical Linear Type Theory Multiplicatives Parallelism and Multicut Extensions 
Lecture 15 Sequent Calculus 

Oct 18  Duality Additives 
Lecture 16  
Week 10  
Oct 23  Additive Extensions Exponential Modalities 
Lecture 17  
Oct 25  Contraction and Weakening Extensions Constructive Classical Logic?! 
Lecture 18  First Half of Homework 3 Due 
Week 11  
Oct 30  Strictness vs. Laziness  Lecture 19  
Nov 1  Effects Monads 
Lecture 20  Second Half of Homework 3 Due 
Week 12  
Nov 6  Effectors Productors 
Lecture 21  
Nov 8  Premonoidal Categories Parallelism 
Lecture 22  
Week 13  
Nov 13  Inductive Types Coinductive Types 
Lecture 23  
Nov 15  (Constructive) Domain Theory  Lecture 24  Homework 4 Due 
Week 14  
Nov 20  Quotient Types  Lecture 25  
Nov 22  No Class Celebrate American Thanksgiving! 

Week 15  
Nov 27  Final Review  Lecture 26  Bring Questions!!! 
Nov 29  Final  Homework 5 Due 
Homework Policies
Cornell University has a Code of Academic Integrity, with which you should be familiar. Violations of this code are treated very seriously by Cornell and can have longterm 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, write up assignments yourself, and if you discuss a problem with another student, you are expected to document this fact in your writeup. It is a violation of the code to copy work, including programs, from other students; it is also a violation to use solutions to homework problems from previous iterations of the same course. Note that Cornell holds responsible for the code violation both the recipient and the donor of improper information.