Instructor: Karl Crary (crary@cs) WeH 8127. Office Hours: By Appointment.
Teaching Assistant: Aleksey Kliger (aleksey@cs) WeH 8114. Office Hours: T 4:00pm -- 5:00pm.
Meeting times: MW 1:30pm -- 2:50pm WeH 5409
We are using Benjamin Pierce's Types and Programming Languages (errata) (Amazon), available in the Campus Store.
The programming language used for projects in the course is Standard ML, using the SML/NJ implementation. If you are new to SML, you may want to read Bob Harper's Programming in Standard ML, as well as the documentation for the SML'97 Basis Library.
You make take the final any 24 hour period during finals week. Copies of the final will be available from Karl's office starting Friday December 6th. Return completed exams to Karl or to Margaret Weigand in 8120. (Note that if you wish to return the exam on Saturday December 7th, you will need to submit it to KArl electronically).
You may use the book or your own notes, however you may not collaborate with others.
A clarification of our (previously implicit) homework policy:
Written assignments are due at the beginning of class on the due date. Programming assignments must be copied to the submission directory by the begining of class, as well.
| Date | Topic | Chapter(s) | Homework |
|---|---|---|---|
| 9 / 11 | Intro / SML | 1 | |
| 9 / 16 | Arithmetic / Syntax / Operational Semantics | 2, 3, 4 | HW 1. Due 9/25: ex. 3.5.17; implement the Arith evaluator (see Ch. 4); recommended (ie, optional) ex. 3.5.16. |
| 9 / 18 | More Operational Semantics. λ-Calculus | 5, 6, 7 | |
| 9 / 23 | More λ-Calculus | ||
| 9 / 25 | Types and Type Safety | 8 | |
| 9 / 30 | Simply Typed λ-calculus | 9, 10 | HW 2. Due 10/9: ex. 5.2.8, 6.2.8, 7.3.1, 6.1.1, 6.2.2, 6.2.5. |
| 10 / 2 | Extensions | 11 | |
| 10 / 7 | Recursive Types | 20 except 20.3 | |
| 10 / 9 | Dynamic Typing | * | HW 3. Due 10/21: ex. 8.3.6, 9.3.2, 9.3.9, 9.3.10, Ch.10(Updated 10/16!: some possible problems and resolutions), Extra Credit: tell us where/how the proof of 9.3.8 cheats. |
| 10 / 14 | References | 13 | |
| 10 / 16 | Exceptions | 14 | |
| 10 / 21 | Abstract Machines and Continuations | * | |
| 10 / 23 | Monads | * | HW 4. Due 11/4. Ex. 11.12.1 (just progress), 20.1.2 (using isorecursive types), 20.2.1 (must do fix, do others if you wish), 20.2.2 (just the "new" cases), extend our previous programming project with isorecursive types. code. |
| 10 / 28 | Polymorphism | 23 | |
| 10 / 30 | ML Polymorphism / Type Inference | 22 | |
| 11 / 4 | Type Inference / Value Restriction | ||
| 11 / 6 | Parametricity | * | |
| 11 / 11 | Existential Types | 24, 25 | HW 5. Due 11/25: ex. 13.5.2, prove preservation for the simply typed lambda calculus with references (that is, the language of figure 13-1 in T&PL), 23.4.9, 23.4.10, 23.4.12, 23.5.2. |
| 11 / 13 | Subtyping | 15 except 15.6, 20.3 | |
| 11 / 18 | Bounded Quantification | 26 | |
| 11 / 20 | Coercive Subtyping | 15.6 | |
| 11 / 25 | Higher-Order Polymorphism | 29, 30, 31 | HW 6. Due Friday 12/6: 15.2.5, 15.3.6, 26.2.2, 26.3.5, 30.3.17, Extra Credit: 30.3.8. |
| 12 / 2 | Curry Howard Isomorphism | ||
| 12 / 4 | Object Encodings | * |
*: Not covered by T&PL. Materials will be provided.
$Log: index.html,v $
# Revision 1.22 2003/08/29 12:23:14 aleksey
# removed homework solutions. email me if you wanted to see them for some reason.
#
# Revision 1.21 2002/11/25 23:02:11 aleksey
# HW 6 is up. Information about the final is available.
#
# Revision 1.20 2002/11/11 16:56:01 aleksey
# homework 5 is up.