CS 510: Schedule

(subject to change at any time)

Week Topic Reading Notes
1 introduction; ML introduction to ML

using SML/NJ

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;


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 2MinML 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.