Announcements
- Students who are not enrolled but are interested in joining the course should fill out this form: https://docs.google.com/forms/d/e/1FAIpQLSfkQgG40cwUsgBx8Dhx8vsZjQU4T-f81Qm_se5JgF8lq3mnwA/viewform?usp=header
- Lecture will be held in Gates 114 and also accessible via Zoom. The Zoom link will be available on CMSX.
- Each student in this course is expected to abide by the Cornell University Code of Academic Integrity. Any work submitted by a student in this course for academic credit must be the student’s own work.
- These web pages are still under development.
Overview
Programming languages are a fundamental part of computer science. This course introduces the formal tools needed to describe precisely what a program means. These tools help us answer many useful questions about program analyses and transformations, such as:
- Is this program correct?
- Will this program encounter a run-time type error?
- Is one program indistinguishable from another?
- Is this optimization a safe program transformation?
- Does this program compute the intended result? Does it leak information?
- Is this compiler translation correct?
- Can source language A be translated into target language B?
- Different styles of dynamic semantics, including operational, axiomatic, and denotational semantics
- Static semantics, especially type systems
- Proofs by induction on derivations and structure
- A formal treatment of important programming language features such as functions, laziness, exceptions, continuations, modules, type polymorphism, objects and classes.
Course Information
Time & Place
Lecture:
- Monday, Wednesday, and Friday, 10:10-11:00am, Gates Hall 114
You are expected to attend all lectures.
Course Staff
| Name/Position | Email/Phone | Office/consulting hours | |
|---|---|---|---|
 |
Andrew Myers 428 Gates Instructor |
[mouse over for email]
(607) 255-8597 |
Mon 3-4pm, Gates 428 |
 |
James Li TA |
[mouse over for email]
|
Wed 1-2pm, Rhodes 408 |
 |
Silei Ren TA |
[mouse over for email]
|
Fri 4-5pm, Rhodes 408 |
Office Hours Weekly Chart
| Day | Name | Time | Location |
|---|---|---|---|
| Monday | Andrew | 3-4pm | Gates 428 |
| Wednesday | James | 1-2pm | Rhodes 408 |
| Friday | Silei | 4-5pm | Rhodes 408 |
Prerequisites
Enrollment limited to: graduate students or permission of instructor. Programming experience and mathematical maturity is required.
Texts
You are required to read the course notes posted on the web site. These will often contain more detail than what was presented in lecture.
Ed
We will be using Ed as an online discussion forum. You are encouraged to post any questions you might have about the course material. The course staff monitor the forum fairly closely and you will usually get a quick response. If you know the answer to a question, you are encouraged to post it, but please avoid giving away any hints on the homework or posting any part of a solution—this is considered a violation of academic integrity.
By default, your posts are visible to the course staff and other students, and you should prefer this mode so that others can benefit from your question and the answer. However, you can post privately so that only the course staff can see your question, and you should do so if your post might reveal information about a solution to a homework problem. If you post privately, we reserve the right to make your post public if we think the class will benefit. You can also post anonymously if you wish not to reveal your identity.
The discussion forum is the most effective way to communicate with the staff and is the preferred mode of interaction. Please reserve email for urgent or confidential matters. Free-ranging technical discussions are especially encouraged. Broadcast messages from the course staff to students will be sent using Ed and all course announcements will be posted there, so check in often.
CMSX
We will be using the course management system CMSX for managing assignments, exams, and grades. Everyone who preregistered for the course should be entered, but if you did not preregister, you are probably missing. Please login here and check whether you exist. There will be a list of courses you are registered for, and CS 6110 should be one of them. If not, please send your full name and Cornell NetID to the course staff so you can be registered.
You can check your grades, submit homework, and request regrades in CMSX. Please check your grades regularly to make sure we are recording things properly. The system also provides some grading statistics. There is a help page with instructions.
Please do not repost course materials released on CMS publicly. These materials are intellectual property and are meant for participants in the course. They are not free to the public.
Announcements and Handouts
Announcements will be posted to Ed. Homework and exam solutions will be available in CMS. Check frequently for new postings.
Assignments & Exams
There will be 4 slip days for assignments this semester, with a 10% per day penalty applied thereafter. Extensions may be granted in case of illness or other acceptable excuse; please contact the course instructor as early as possible if an extension will be needed.
There will be a 1½-hour evening prelim and a 2½-hour final exam. Please check the schedule page for times and locations.
Your final grade will be based on your assignment and exam scores according to the following weights:
| Participation | 3% | |
| Assignments | 47% | |
| Assignment 1 | 8% | |
| Assignment 2 | 8% | |
| Assignment 3 | 9% | |
| Assignment 4 | 9% | |
| Assignment 5 | 9% | |
| Assignment 6 | 4% | |
| Prelim | 20% | |
| Final | 30% | |
Participation will be assessed based on attendance and participation in class, participation in Ed discussions, filling out course evaluations, and pop quizzes given in class (usually promptly at the start!)
Scores will be averaged by computing a weighted quadratic mean, which means that unrepresentatively low scores (such as missing assignments) will have less weight.
Regrades
Homework regrade requests can be submitted electronically in CMS. Exam regrades should be handwritten and submitted to the course staff. Please include a description of the grading error with your regrade request.
Academic Integrity
Each student in this course is expected to abide by the Cornell University Code of Academic Integrity. Any work submitted by a student in this course for academic credit must be the student’s own work.
A high level of academic integrity is expected of all students. Under no circumstances may you submit work done with or by someone else under your own name or share detailed proofs or code with anyone else except your partner. However, discussions about general techniques or the requirements of the assignment are permissible.
You must cite all sources, including Internet sources. You must acknowledge by name anyone whom you consulted (excluding course staff). You may not give nor receive assistance from anyone else during an exam. You may not post any material that might be part of a solution publicly on Ed. If your question necessarily includes such material, post privately.
If you are unsure about what is permissible and what is not, please ask.
Academic Integrity Resources:
- • Cornell University Code of Academic Integrity
- • Computer Science Department Code of Academic Integrity
- • Explanation of AI Proceedings
Special Needs
We will provide appropriate accommodation for students with special needs or disabilities. Requests for accommodation are to be made during the first three weeks of the semester and must be accompanied by official documentation. Please register with Student Disability Services in 110 Ho Plaza (Cornell Health Building), Level 5 to document your eligibility.
All dates for lectures and unreleased assignments are provisional. Notes from Spring 2009 and Spring 2010 are likely to be close approximations.
| Lecture | Date | Topic/notes | Readings | Assignments, etc. | |
|---|---|---|---|---|---|
| 1 | Jan 24 | Course overview | Pierce Ch. 1-2 | ||
| Operational semantics | |||||
| 2 | Jan 27 | Lambda calculus | Pierce Ch 5.1-2 | ||
| 3 | 29 | Lambda calculus encodings, CBV and CBN semantics | Pierce 5.3-4 | HW1 out 1/30 | |
| 4 | 31 | Substitution, big-step vs. small-step SOS | Pierce 3.1-2,4-5 | ||
| 5 | Feb 3 | Imperative semantics: IMP | Pierce 3.3,6, Winskel Ch 2 | ||
| 6 | 5 | Inductive definitions | Winskel 3.1-3 | (2/4 add deadline) | |
| 7 | 7 | Well-founded induction | Winskel 4.1-4, Pierce 21.1 | ||
| 8 | 10 | Rule induction, evaluation contexts | Winskel 4.1-4, Pierce 21.1 | HW1 due | |
| 9 | 12 | Semantics by translation, adequacy discussion 1: OCaml review (Statler 291, 7pm Monday) discussion 2: OCaml review (Statler 291, 7pm Tuesday) |
|||
| 10 | 14 | Strong typing | |||
| Feb 17 | February break | ||||
| Language features | |||||
| 11 | Feb 19 | Naming and scope | |||
| 12 | 21 | Recursive bindings and modules | |||
| 13 | 24 | State and mutable variables, pass by reference | |||
| 14 | 26 | Continuation-passing style | HW2 due | ||
| 15 | 28 | Compiling with continuations | |||
| 16 | Mar 3 | Closure conversion and lambda lifting | [video] | HW3 out | |
| 17 | 5 | Errors and exceptions in CPS | |||
| 18 | 7 | State in CPS and first-class continuations | |||
| Axiomatic semantics | |||||
| 19 | Mar 10 | Hoare logic | Winskel 6 | ||
| 20 | 12 | Predicate transformers | Winskel 7 | ||
| Denotational semantics | |||||
| 21 | Mar 14 | Denotational semantics of IMP | Winskel 5 | ||
| 22 | 17 | The Fixed-Point Theorem | Winskel 5 | HW3 due | |
| 23 | 19 | Domain constructions | Winskel 8 | (3/18 drop deadline) | |
| 21 | Preliminary examination | ||||
| Mar 21 | Prelim (in-class) | ||||
| 24 | 24 | Denotational semantics of recursive functions | Winskel 9 | ||
| Types | |||||
| 25 | Mar 26 | Simply typed lambda calculus | Pierce 8.1–2, 9.1–2, 9.5–9.6, 10.1–3, Winskel 11.1–3 | HW4 out | |
| 26 | 28 | Products, sums, and more | Pierce 11.1-10, Winskel 11.11 | ||
| Mar 31 | Spring break | ||||
| Apr 2 | Spring break | ||||
| Apr 4 | Spring break | ||||
| 27 | Apr 7 | Soundness of the type system | Pierce 8.3, 9.3, Winskel 11.9 | ||
| 28 | 9 | Subtype polymorphism | Pierce 15.1-6 | ||
| 29 | 11 | Proof normalization and minimal typing | Pierce 16 | ||
| 30 | 14 | Strong normalization and logical relations | Pierce 12 | HW4 due | |
| 31 | 16 | Propositions as types | Pierce 9.4, Wadler | ||
| 32 | 18 | Type inference | Pierce 22.1-5 | ||
| 33 | 21 | Parametric polymorphism | Pierce 22.6-7, 23 | ||
| 34 | 23 | Recursive types | Pierce 20, Winskel 13 | ||
| More domain theory | |||||
| 35 | Apr 25 | Solving domain equations with D∞ | Winskel 12, Mitchell 7 | ||
| 36 | 28 | Monads, nondeterminism and powerdomains | HW5 due 4/29 | ||
| 37 | 30 | Abstract interpretation | |||
| Advanced features | |||||
| 38 | May 2 | Existential types | Pierce 24, CW86 | ||
| 39 | 5 | Higher-order polymorphism | Pierce 29-30, PJM97, Sec. 3 | HW6 due 5/6 | |
| May 6 | HW6 due | ||||
| May 11 | Final exam, 9:00AM-11:30AM, Gates Hall G01 | ||||
Resources
Course notes
Course notes for individual lectures and recitations can be found on the course schedule.
Useful textbooks
The following books are recommended but not required:
- Types and Programming Languages: Benjamin Pierce
- Formal Semantics of Programming Languages, Glynn Winskel
Some other useful texts that provide a different perspective or more depth in some areas are:
- Programming Languages: Theory and Practice, by Robert Harper (online draft)
- Foundations for Programming Languages, by John Mitchell
- Semantics for Programming Languages, by Carl Gunter
- Basic Category Theory for Computer Scientists, by Benjamin Pierce
Online resources for OCaml:
- OCaml home page
- OCaml textbook
- OCaml from the Very Beginning, a gently paced introduction to OCaml.
- F#, a language similar to OCaml. You can use the Visual Studio IDE to write and debug F# programs.
- OCaml support for emacs and vim
- ledit, a tool to provide emacs-like editing (and history) to the OCaml toplevel. (Info on how to use ledit, and other tips for using the toplevel, here.)
Other useful code
Assignments
All source code will be available on CMS.
| Homework 1 |
| Homework 2 |
| Homework 3 |
| Homework 4 |
| Homework 5 |
| Homework 6 |