Updates
(12-11) Lecture notes (TeX source) for November 14 and 16 are available. Thanks to John for scribing!
(12-10) Lecture notes (TeX source) for December 5 and 7 are available. Thanks to Kanat for scribing! (Note: You will not be responsible for this material on the final --- it is provided only for your curiosity.)
(12-9) Lecture notes for November 7 and 9 (source, thanks to Wenjie!) and November 21, 28, and 30 (source, thanks to Jason!) are available.
Additionally, some notes on existentials (source) are available. This material was covered October 31.
(12-1) Homework 5 is up (handout, TeX source). This assignment is written-only, so there's no code tarball. It's due December 7, the last day of lecture.
(11-26) Lecture notes (source) for October 26 are available. Thanks to Hormoz for scribing!
(11-20) Lecture notes (source, figure) for October 17 and October 19 are available. Thanks to Kami for scribing!
(11-18) Homework 4 is up (handout, TeX source, code). It's due the Tuesday after Thanksgiving.
(10-28) Homework 3 is up (handout, TeX source, code). It's due Thursday, November 9, but don't put it off---it's a bit heavier on programming than the first two assignments.
(10-20) Lecture notes (source) for October 10 and October 12 are available. Thanks to Xinyu for scribing!
(10-15) Lecture notes (source) for October 3 and October 5 are available. Thanks to Dash for scribing!
(10-11) Homework 2 is up (handout, TeX source, code)
(10-07) Lecture notes (source) for September 26 and September 28 are available. Thanks to Tunji for scribing!
(9-28) Lecture notes (source) for September 19 and September 21 are available. Thanks to Fritz for scribing!
(9-22) Lecture notes for September 12 and September 14 are available. Thanks to Kyung-Ah for scribing them! (LaTeX source is also available)
(9-22) SML examples from the SML introduction lectures are online.
- Welcome to 15-814!
References
Primary
| Robert Harper, Practical Foundations for Programming Languages , Working draft, Fall, 2006. |
| Benjamin C. Pierce, Types and Programming Languages , MIT Press, 2002. |
| Benjamin C. Pierce, ed., Advanced Topics in Types and Programming Languages , MIT Press, 2005. |
Secondary
| Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction , MIT Press, 1996. |
| John C. Reynolds, Theories of Programming Languages , Cambridge University Press, 1998. |
| John C. Mitchell, Foundations for Programming Languages , MIT Press, 1996. |
Software
The programming language used for projects in the course is Standard ML, using the Standard ML of New Jersey (SML/NJ) implementation. For further information, you may want to read Programming in Standard ML, as well as the documentation for the Standard ML Basis Library.
A stable version of SML/NJ may be installed on facilitized machines using the misc collections. Please note that the compilation manager in versions 110.43 and beyond is not compatible with that of earlier versions of the compiler.
Many of the lecture notes use Didier Rémy's mathpartir LaTeX package.
Homework
You are required to achieve a grade of B on each homework assignment. If, after grading, your assignment does not meet this standard, you are required to re-submit within one week a revised solution that corrects any errors or omissions to achieve a grade of B. This policy ensures that the emphasis is properly on learning the course material, and not on "getting through it."
All homeworks are due at the beginning of lecture on the due date. All homeworks are to be submitted by copying them to your submission directory in /afs/cs/academic/class/15814-f06/handin. Written homeworks are to be submitted in PDF format (only!), and must be typeset for the sake of legibility. The form of submission for a programming assignment is given with the assignment.
Note Taking
Everyone is required to participate in the note-taking cooperative. Students are to form themselves into groups of two or three (depending on enrollment), so that each group is responsible for preparing the notes for one week of the semester. Each week the responsible group will take notes, typeset them in a form suitable for use by the other students, and submit them for approval (and possible instructions for revision) by the teaching assistant. The first draft is due Monday morning of the following week, and the final draft is to be published on the web site by Wednesday morning of the same week. Notes must be typeset with LaTeX using the template provided.
The note-taking schedule is now online.
Final Exam
There will be a 24-hour take-home final examination during the final exam period at the end of the semester.
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 must be erased, and you must not transcribe or take with you anything that has been written on the board during your discussion. You must be able to reproduce the results solely on your own after any such discussion.
Grading
C. S. Ph.D students are assigned a pass/fail grade in the University grading system, but are given an internal letter grade for Black Friday purposes. A final letter grade of B is required to pass this course. To achieve this, you must have (1) completed all homework assignments with a grade of B; (2) earned a grade of B or better on the final exam; (3) prepared lecture notes to the standard required by the teaching assistant.
Undergraduate students and students in other programs will be assigned letter grades according to the same policies used to assign internal letter grades for C.S. Ph.D. students just outlined.
Schedule of Lectures
| Date | Topic | Chapters | Notes | Homework | ||
|---|---|---|---|---|---|---|
| Sep | 12 | Overview, Inductive Definitions | TAPL 1-4; PFPL 1-2 | |||
| 14 | Abstract Syntax and Binding | PFPL 4-8 | Lecture notes (9/12,14) (Source) | |||
| 19 | Programming in SML | SML Examples | ||||
| 21 | Untyped λ-Calculus | TAPL 5 | Lecture notes (9/19,21) (Source) | Homework 1 out (handout [source], code) | ||
| 26 | λ-Definable Functions | TAPL 5 | ||||
| 28 | Church-Rosser Theorem, Reduction Strategies | TAPL 5 | Lecture Notes (9/26, 9/28) (Source) | |||
| Oct | 3 | Goedel's T, Type Safety | TAPL 8, 9, 12, PFPL 16 | |||
| 5 | Termination; Plotkin's PCF | TAPL 11, PFPL 17 | Lecture Notes (10/3, 10/5) (Source) | Homework 1 due | ||
| 10 | Plotkin's PCF; Sums and Products | TAPL 11, PFPL 17 | Homework 2 out (handout [source], code) | |||
| 12 | Recursive Types | TAPL 11, PFPL 21 | Lecture Notes (10/10, 10/12) (Source) | |||
| 17 | Subtyping, Variance | TAPL 15, 16, PFPL 32 | Homework 2 due | |||
| 19 | Subtyping Recursive Types | TAPL 20, 21, PFPL 32 | Lecture Notes (10/17, 10/19) (Source, figure) | |||
| 24 | (class cancelled) | Homework 1 re-do due | ||||
| 26 | Polymorphic Types; Church Encodings | TAPL 22-23, PFPL 24 | Lecture Notes (10/26) (Source) | Homework 3 out (handout [source], code) | ||
| Oct | 31 | Existential Types; Abstract Types | TAPL 24, PFPL 25 | Lecture Notes (10/31) (Source) | ||
| Nov | 2 | Propositions and Types | TAPL 9.4, PFPL 30 | |||
| 7 | Control Effects: Exceptions | TAPL 14, PFPL 27 | Homework 2 re-do due | |||
| 9 | Control Effects: Continuations | PFPL 28 | Lecture Notes (11/7, 11/9) (Source) | Homework 3 due | ||
| 14 | Classical Logic and Control | PFPL 31 | ||||
| 16 | Store Effects: References | TAPL 13, PFPL 33 | Lecture Notes (11/14, 11/16) (Source) | Homework 4 out (handout [source], code) | ||
| 21 | Store Effects: Monads | PFPL 34 | ||||
| 23 | (Thanksgiving) | |||||
| 28 | Lazy Evaluation | PFPL 36-37 | Homework 3 re-do due, Homework 4 due | |||
| 30 | Module Systems | ATTAPL 8, PFPL 43 | Lecture Notes (11/21, 11/28, 11/30) (Source) | Homework 5 out (handout [source]) | ||
| 5 | Dependent Types | ATTAPL 2 | Homework 4 re-do due | |||
| 7 | Logical Frameworks | Lecture Notes (12/5, 12/7) (Source) | Homework 5 due | |||