15-814 Types and Programming Languages

Course Information

Time: Mon-Wed 12:00 pm - 1:20 pm
Room: 4303 GHC
Instructor: Karl Crary
Teaching Assistant: Ankush Das
Discussion Board: Piazza Page
Office Hours
Karl Crary: Mon 4 pm - 5 pm 9217 GHC
Ankush Das: Fri 1 pm - 3 pm 9225 GHC


This is an introductory course on the foundations of programming languages. The central organizing principle is the identification of language features with types. The theory of programming languages, therefore, reduces to the theory of types. Type theory is a comprehensive foundational theory of computation, and also corresponds (in a way that can be made mathematically precise) to the vernacular of logic. The course is about the dual interpretations of type theory as programming and as logic, and about the interplay between those interpretations.


Robert Harper,
Practical Foundations for Programming Languages (Second Edition),
Cambridge University Press, April 2016.
[Online Preview]


You are required to achieve a grade of B on each homework assignment. If you receive a C or D on an on-time submission, you will be given extra time in which to revise to achieve a B grade on that assignment. Failure to submit on time, or a failing grade on an assignment, precludes resubmission and will result in a failing grade in the course.

All homeworks are due by 11 pm on the stated due date. No late homeworks will be accepted, unless prior permission is obtained from the instructor, which will be granted only under exceptional circumstances. Homeworks are to be submitted by email to the teaching assistant. Homeworks should preferably be typeset in LaTeX, but can also be handwritten neatly, scanned and submitted as a PDF.

All homeworks are to be submitted by sending the PDF via e-mail to the teaching assistant with "15-814 Homework" as the subject line. No late homeworks will be accepted. Any re-do's must be finished within three days of their being returned to you. One re-do is generally permitted per assignment. You would be allowed more than one re-dos only under exceptional circumstances.

Midterm Exam

There will be a 24-hour take-home midterm examination during the exam period in the mid of semester. You will be assigned a letter grade as for homework.

Final Exam

There will be a 24-hour take-home final examination during the exam period at the end of semester. You will be assigned a letter grade as for homework.

Academic Integrity

Unless explicitly instructed otherwise, all homework and exam work is to be solely your own, and may not be shared with or borrowed from any other person in the course. You are not permitted to draw upon assignments or solutions from previous instances of the course, nor to use course materials (such as assignments or programs) obtained from any web site or other external source in preparing your work.

You may discuss homework assignments with other students in the class, but you must adhere to the whiteboard policy. At the end of discussion the whiteboard (or whatever discussion medium is used) must be erased, and you must not transcribe or take with you anything that has been written on the board during your discussion. In other words, after any such discussion, you must be able to reproduce the results solely on your own.

Tentative Schedule of Lectures

Date Topic Reading Homework
Sep 5 Labor Day (No lecture)
7 What is a programming language? PFPL1-7
12 Rule Induction HW1 out
(handout [LaTeX template] [macros])
14 Type Safety PFPL8-11
19 Lambda Calculus
21 PFPL 14-15
26 Products and Sums
28 System T PFPL 16-17, 49 HW1 due (solutions)
HW2 out
(handout [LaTeX template] [macros])
Oct 3 Inductive Types Notes on inductive types
5 Polymorphism and System F PFPL 19-20 HW2 due (solutions)
10 Abstraction Theorem HW3 out
(handout [LaTeX template] [macros])
12 Data Abstraction PFPL 22-23
17 Free Theorems HW3 due (solutions)
HW4 out
(handout [LaTeX template] [macros])
19 PCF and Recursive Types PFPL 26
24 Curry-Howard Isomorphism
26 State and Effects PFPL 37-38
31 Modernized Algol HW4 due (solutions)
Nov 2 Assignables and References PFPL 28-30 HW5 out
(handout [LaTeX template] [macros])
7 Subtyping
9 Control Stacks PFPL 34
14 Exceptions and Continuations
16 Higher Kinds PFPL 35 HW5 due (solutions)
HW6 out
(handout [LaTeX template] [macros])
21 Linear Logic PFPL 36
23 Thanksgiving!
28 Applications of Linear Logic
30 Resource Analysis
TA Lecture
HW7 out
(handout [LaTeX template] [macros])
Dec 5 Logical Frameworks PFPL 39-40 HW6 due (solutions)
7 Ordered and Modal Logic HW7 due (solutions)

Ankush Das

Valid XHTML 1.0 Strict

Valid CSS