CS 510: Schedule
(subject to change at any time)
| Week | Topic | Reading | Notes |
|---|---|---|---|
| 1 | introduction; ML | introduction
to ML
Pierce 4 |
course-intro,
ML-intro,
intro2
|
| 2 | inductive definitions; syntax, scope, substitution | Pierce (skim 2),3,5 | inductive defs, lambda calculus |
| 3 | typed lambda calculus, MinML | Pierce 1,8 | dynamics, statics |
| 4 | type safety, typing data structures | Pierce 9, 11 | safety, sums & products |
| 5 | recursive types, exceptions | Pierce 20-20.2; Pierce 14 | recursive types, exceptions |
| 6 | references and stateful programming languages | Pierce 13; Harper 10 | references, tinyC |
| mid-term break | |||
| 7 | midterm handed
out;
dynamic typing; polymorphism |
Harper 24; Pierce 23 | dynamic typing; polymorphism |
| 8 | existentials; type inference | Pierce 24; Pierce 22 | existential types; type inference |
| 9 | type inference; subtyping | Pierce 22; Pierce 15 | subtyping |
| 10 | algorithmic subtyping | Pierce 16 | algorithmic subtyping |
| 11 | Java | Pierce 19 | FJ; Java |
| 12 | continuations; linear typing | Harper ; Walker | continuations; continuations 2; |
Acknowledgement: Many 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.