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.
We are using Benjamin Pierce's Types and Programming Languages (errata) (Amazon), available in the CMU Bookstore.
The programming language used for projects in the course is Standard ML, using the SML/NJ implementation. You may wish to review the slides from our Introduction to SML. For further information, you may want to read Bob Harper's Programming in Standard ML, as well as the documentation for the SML'97 Basis Library.
A stable version of SML/NJ may be installed on facilitized machines using the misc collections. If you wish to install a copy of the software on your own (non-facilitized) machine, please install 110.0.7. Note that in the latest SML/NJ working version (110.43), the Compilation Manager (CM) underwent a redesign. As a result, there might be incompatabilities in later programming assignments between 110.0.7 and 110.43.
Both written and programming assignments are due at the beginning of lecture on the due date. Programming assignments must be copied to the submission directory, while written assignments will be collected in class.
The final exam will be a 24 hour take-home exam. You may start at any time during the first week of finals. You may pick up the exam from Karl. If you're planning on picking it up outside of regular business hours, please make arrangements in advance by email.
If you plan on returning the exam over the weekend, you should return it by email. Otherwise hand the exam back to Karl within 24 hours.
| Date | Topic | Chapters | Homework |
|---|---|---|---|
| 9/2 | Intro | 1 | |
| 4 | Syntax & Semantics | 2,3,4 | |
| 9 | Operational Semantics; λ-calculus | 5,6,7 | Hw#1, due 9/16: 3.5.17, Port Chapter 4 to SML. Recommended: 3.5.16 |
| 11 | (cont'd) (encoding booleans in the λ-calculus) | ||
| 16 | (cont'd) (encoding natural numbers, recursion) | ||
| 18 | (cont'd) (substitution); Types & Type Safety | 8 | Hw#2, due 10/2: 5.2.8, 6.2.8, 7.3.1 (programming assignment), 6.1.1, 6.2.2, 6.2.5. Recommended: 6.2.7, 6.3.1 |
| 23 | (cont'd) (Safety, Progress, Canonical Forms, Preservation for typed Arith) | ||
| 25 | Simply-typed λ-calculus | 9,10 | |
| 30 | (cont'd) | ||
| 10/2 | Expressions & Derived Forms | 11 | Hw#3, due 10/16: 8.3.6, 9.2.2, 9.3.2, 9.3.9 extended with products (show just the lambda and application, and pairing and projection cases of the proof), 9.3.10, Port Chapter 10 extended with nats and unit to SML |
| 7 | (cont'd) | ||
| 9 | Recursive types | 20, except 20.3 | |
| 14 | (cont'd); References | 13 | |
| 16 | (cont'd) | Hw#4, due 10/30: see above. | |
| 21 | Polymorphism | 23 | |
| 23 | (cont'd) | ||
| 28 | Parametricity | [papers] | |
| 30 | (cont'd) | Hw#5, due 11/13: 13.5.2, preservation thm for refs (incl relevant store lemmas), 23.4.9, 23.4.10, 23.4.12, 23.5.2 | |
| 11/4 | Existential types | 24,25 | |
| 6 | (cont'd) | ||
| 11 | Subtyping | 15, except 15.6 | |
| 13 | (cont'd) | ||
| 18 | Bounded Quantification | 26 | Hw#6 out (see above). Due 12/4 |
| 20 | (no class) | ||
| 25 | Curry-Howard Isomorphism | [handout] | |
| 12/2 | Substructural logics | [paper] | |
| 12/4 | (cont'd) | Homework 6 solution available: .ps, .pdf |
The latter paper is worth reading at least for the fable in the introduction.
$Log: index.html,v $ # Revision 1.17 2003/11/19 15:36:35 aleksey # I made a typo. Problem set #6 includes problem 15.3.6, not 25.3.6 # # Revision 1.16 2003/11/18 15:24:26 aleksey # Hw 6 is up. Also, info about final exam. # # Revision 1.15 2003/10/30 22:28:27 aleksey # hw5 is up # # Revision 1.14 2003/10/27 16:55:13 aleksey # revised schedule
