15814 Types and Programming Languages
Course Information
Date / Time:  Mon & Wed / 12:00 pm  1:20 pm  
Room:  GHC 4303  
Instructor:  Karl Crary  
Teaching Assistant:  Yong Kiam Tan  
Discussion Board:  Piazza Page  
Office Hours  
Karl Crary:  Tue / 3:30 pm  4:30 pm  GHC 9217 
Yong Kiam:  Thu / 4:00 pm  5:00 pm  GHC 7513 
Synopsis
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.
Text
Robert Harper, Practical Foundations for Programming Languages (Second Edition), Cambridge University Press, April 2016. 
[Online Preview] 
Homework
You are required to achieve a grade of B on each homework assignment. If you receive a C or D on an ontime 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 email to the teaching assistant with "15814 Homework" as the subject line. No late homeworks will be accepted. Any redo's must be finished within three days of their being returned to you. One redo is generally permitted per assignment. You would be allowed more than one redos only under exceptional circumstances.
Midterm Exam
There will be a 24hour takehome 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 24hour takehome 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  4  Labor Day (No lecture)  
6  Inductive Definitions  PFPL 13  
11  Statics and Dynamics  PFPL 45 
HW1 out
(handout [LaTeX template] [macros] ) [solutions] 

13  Type Safety  PFPL 6  
18  SimplyTyped Lambda Calculus  PFPL 8, 21  
20  Substitution  PFPL 8, 21  
25  Contextual and Evaluation Dynamics Products and Sums 
PFPL 5.3, 7 PFPL 10, 11 
HW1 due HW2 out (handout [LaTeX template] [macros]) [solutions] 

27  System T  PFPL 9  
Oct  2  Definability  PFPL 9  
4  Polymorphism and System F  PFPL 16  
9  Existential Types Data Abstraction 
PFPL 17 PFPL 48 
HW2 due HW3 out (handout [LaTeX template] [macros]) [solutions] 

11  Abstraction Theorem  PFPL 48  
16  Free Theorems  Theorems for free!  HW3 due HW4 out (handout [LaTeX template] [macros]) [solutions] 

18  CurryHoward Isomorphism  
23  PCF and Recursive Types  PFPL 1920  Midterm (available 23 Oct  27 Oct)  
25  State and Effects  PFPL 34  
30  Modernized Algol  PFPL 3435  HW4 due HW5 out (handout [LaTeX template] [macros]) 

Nov  1  Modernized Algol  PFPL 3435  
6  Assignables and References  PFPL 3435  
8  Control Stacks  PFPL 28  
13  Exceptions and Continuations  PFPL 2930  HW5 due  
15  Continuations and Classical Logic  PFPL 13 
HW6 out
(handout [LaTeX template] [macros]) 

20  Linear Logic  
22  TBD  
27  Applications of Linear Logic  
29  TBD  
Dec  4  Logical Frameworks  HW6 due  
6  Ordered and Modal Logic 