Final grades are posted on Canvas.
Assignment I, handed out on 1/8 and due on 1/22
Assignment II, handed out on 1/24 and due on 2/5
Assignment III, handed out on 2/19 and due on 2/26
Assignment IV, handed out on 2/28 and due on 3/19
Assignment V, handed out on 3/19 and due on 4/9
Assignment VI, handed out on 4/9 and due on 4/23
Please use Canvas to check your grades.
Textbook webpage (including errata)
Proofs are Programs: 19th Century Logic
and 21st Century Computing
by Philip Wadler (2000).
This optional reading briefly covers the works of Frege, Gentzen, and Church, as well as the Curry-Howard Isomorphism.
|Week||Dates||Topics||Reading (ML book)|
|1||01/08, 01/10||Introduction; ML basics; Polymorphism||1-3.1, 5.3|
|2||01/17||Functions; Patterns||3.2-3.6.3, 4.1-4.2|
|3||01/22, 01/24||Functions||5.1, 5.4-5.6|
|4||01/29, 01/31||Datatypes; Deductive systems||6.1-6.3|
|5||02/05, 02/07||Deductive systems; Syntax||Class notes|
|6||02/12, 02/14||Test I||Class notes|
|7||02/19, 02/21||Syntax; Dynamic semantics||Class notes|
|8||02/26, 02/28||Dynamic semantics; Lambda calculus||Class notes|
|9||03/05, 03/07||Lambda calculus; Static semantics||Class notes|
|10||03/19, 03/21||Type safety||Class notes|
|11||03/26, 03/28||Test II||Class notes|
|12||04/02, 04/04||Type safety; Algebraic data types||Class notes|
|13||04/09, 04/11||Recursive types; Side effects||5.2, 7.2-7.3|
|14||04/16, 04/18||Side effects||Class notes|
|15||04/23, 04/25||Side effects||Class notes|
|Final||04/30||Test III (Final Exam), 3-5pm||All tests are cumulative|