CS 510: Schedule
(subject to change at any time)
| Week | Topic | Reading | Notes |
|---|---|---|---|
| 1 | introduction; ML | introduction to ML | introduction,
ML1, ML2
|
| 2 | inductive definitions; syntax, scope, substitution | Harper 1,3,4,5 | inductive def, syntax, hoas |
| 3 | MinML; static and dynamic semantics; type safety | Harper 6,7,8,9 | MinML statics, MinML dynamics, MinML_safety |
| 4 | products; sums; recursive types; dynamic typing | Harper 19, 24 | sum/prod, rec_type, dynamic_types |
| 5 | abstract machines; MinML references; | Harper 11, 14 | abst machines, effects |
| 6 | tinyC; exceptions; continuations; CPS; co-routines | Harper 10, 13 | tinyC, continuations, co-routines |
| mid-term break | |||
| 7 | midterm handed
out;
PolyMinML |
Harper 20 | poly |
| 8 | existential types; data abstraction; type inference | Harper 21, 30 | adts, exists, type inference 1 |
| 9 | type inference; subtyping; coercions | Harper 26, Pierce notes | type inference 2; MinML subtyping; coercions |
| 10 | Java and Featherweight Java | Harper 25, 27, Pierce notes | inheritence; FJ |
| 11 | concept review; concurrency | Reppy notes | midterm review; concurrency |
| 12 | concurrency; Curry-Howard isomorphism | Reppy notes; Wadler Paper | cml programming; cml impl.; proofs-programs |
Acknowledgement: Most of the notes listed above are taken directly from a course taught by Robert Harper at Carnegie Mellon University. I greatly appreciate Bob's generous donation of these resources.