| Time: | Mon/Wed 10:30-11:50 |
| Room: | 4615A Wean Hall |
| Instructor: | Karl Crary |
| Teaching Assistant: | Paul Zagieboylo |
| Office Hours |
|
| Crary: | TBD Wean 8127 |
| Zagieboylo: | Tues 16:30-18:00 Wean 3723 |
The course studies the theory of type systems, with a focus on applications of type systems to practical programming languages. The emphasis is on the mathematical foundations underlying type systems and operational semantics. The course includes a broad survey of the components that make up existing type systems, and also teaches the methodology behind the design of new type systems.
The sixth and last homework assignment is due on the last day of classes, 7 December 2007, by 17:30 EST. It consists of the problems (from TaPL) 15.2.5 and 15.3.6. It also contains an extra problem [pdf] [ps] [LaTeX] or two created by the course staff.
There is some supplemental reading for the next week of lecture. By Wednesday, 14 November, please read Theorems for free by Philip Wadler.
The fifth homework assignment consists of the problems (from TaPL) 13.5.2, 23.4.9, 23.4.10, 23.4.12, 23.5.2, and proving preservation for references as presented in section 13.5 (essentially, flesh out the proof of theorem 13.5.3; please only do the cases that talk about references).
The fourth homework assignment is due on Wednesday, 7 November 2007, at the beginning of class. It consists of the problems 11.12.1 (please only do the progress portion), 20.1.2 (but use isorecursive types for practice), and 20.2.2 (but only do the roll (fold) and unroll (unfold) cases, the others are uninteresting). There is no programming portion for this assignment.
By popular demand, a signature and starter file for the programming part of homework assignment 3 have been produced. They really don't contain anything that you shouldn't have been able to come up with on your own, but here you are. They're in /afs/andrew/course/15/814/handout/hw3/.
The third homework assignment is due on Monday, 22 October 2007 at the beginning of class. It consists of the problems (from TaPL) 8.3.6, 9.2.2, 9.3.2, 9.3.9, 9.3.10, and porting Chapter 10 to SML, with the addition of a new base type unit. It is also recommend to decide what weaselly thing occurs in the proof of lemma 9.3.8. A signature for chapter 10 will be released soon.
The sample solution for homework assignment 1 has been released, in pdf and ps form. You can also get my LaTeX source if you're curious how to perform any particular bit of typesetting.
A signature and starter file for homework assignment 2 have been made available. You can find them in /afs/andrew/course/15/814/handout/hw2/. Submissions not containing a structure Hw2 that ascribes to the signature HW2 as provided in hw2.sig will not be considered for credit.
The second homework assignment is due on Monday, 8 October at the beginning of class. It consists of the problems (from TaPL) 5.2.8, 6.1.1, 6.2.2, 6.2.5, 6.2.8, and 7.3.1 (programming). It is also recommended to work through 6.2.7 and 6.3.1 if you have the time.
If you don't have the LaTeX proof or code packages, now you do. See the LaTeX page for further tips.
For those who didn't get it, the first homework assignment is due Wednesday, 26 September. The assignment consists of problem 3.5.17 from TaPL and porting the integer arithmetic simulator in Chapter 4 of TaPL to SML.
The SML crash course will be on Thursday, 20 September, at 18:30 EDT in Wean 4623.
Welcome to 15-814! The website is now up, and you've found it!
| Benjamin C. Pierce, Types and Programming Languages , MIT Press, 2002. |
| Robert Harper, Practical Foundations for Programming Languages , Working draft, Fall, 2006. |
| Benjamin C. Pierce, ed., Advanced Topics in Types and Programming Languages , MIT Press, 2005. |
| 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. |
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.
You should learn LaTeX. For Windows, I recommend MikTeX and TeXnicCenter; in Linux, your editor of choice certainly has a LaTeX package and mode of some sort. A decent LaTeX primer can be found here. I'll add more as I find them.
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. Written homeworks are to be typeset for the sake of legibility. Programming assignments should be submitted to your handin directory in /afs/andrew/course/15/814/handin/.
There will be a 24-hour take-home final examination during the final exam period at the end of the semester.
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.
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.
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.
| Date | Topic | Chapters | Homework | |
|---|---|---|---|---|
| Sep | 10 | Intro | TaPL 1 | |
| Sep | 12 | Syntax and Semantics | TaPL 2,3,4 | |
| 17 | λ-Calculus, Part I | TaPL 5,6,7 | ||
| 19 | λ-Calculus, Part II | |||
| 24 | λ-Calculus, Part III | |||
| 26 | Types and Type Safety, Part I | TaPL 8 | Assignment 1 due | |
| Oct | 1 | Types and Type Safety, Part II | ||
| 3 | Simply Typed λ-Calculus, Part I | TaPL 9, 10 | ||
| 8 | Simply Typed λ-Calculus, Part II | |||
| 10 | Extensions and Derived Forms, Part I | TaPL 11 | ||
| 15 | Extensions and Derived Forms, Part II | |||
| 17 | Recursive Types | TaPL 20, except 20.3 | ||
| 22 | References, Part I | TaPL 13 | ||
| 24 | References, Part II | |||
| 29 | Continuations, Part I | Handout | ||
| 31 | Continuations, Part II | |||
| Nov | 5 | Polymorphism, Part I | TaPL 23 | |
| 7 | Polymorphism, Part II | |||
| 12 | Parametricity | Handout | ||
| 14 | Existential Types | TaPL 24, 25 | ||
| 19 | Subtyping, Part I | TaPL 15 except 15.6; TaPL 20.3 | ||
| 26 | Subtyping, Part II | |||
| 28 | Bounded Quantification | TaPL 26 | ||
| Dec | 3 | Curry-Howard Isomorphism, Part I | Handout | |
| 5 | Curry-Howard Isomorphism, Part II | |||