Final grades are posted on Canvas.
Assignment I, handed out on 1/13 and due on 1/24
Assignment II, handed out on 1/25 and due on 2/7
Assignment III, handed out on 1/25 and due on 2/8
Assignment IV, handed out on 2/8 and due on 2/28
Assignment V, handed out on 2/8 and due on 2/29
Assignment VI, handed out on 3/2 and due on 3/20
Assignment VII, handed out on 3/2 and due on 3/21
Assignment VIII, handed out on 3/21 and due on 4/24
Assignment IX, handed out on 3/21 and due on 4/25
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.
SML# in industry: a practical ERP system development
by Ohori et al. (2014)
This optional reading describes experiences using an ML-style language to develop business software.
(This paper should be accessible on campus; off campus you might try searching for the paper's title.)
|Week||Dates||Topics||Reading (in ML book)|
|1||01/11, 01/13||Introduction; ML basics; Polymorphism||1-3.1, 5.3|
|2||01/20||Functions; Patterns||3.2-3.6.3, 4.1-4.2|
|3||01/25, 01/27||Functions||5.1, 5.4-5.6|
|4||02/01, 02/03||Datatypes; Deductive Systems||6.1-6.3|
|5||02/08, 02/10||Deductive Systems; Syntax||Class notes|
|6||02/15, 02/17||Test I||Class notes|
|7||02/22, 02/24||Syntax; Dynamic semantics||Class notes|
|8||02/29, 03/02||Lambda calculus||Class notes|
|9||03/07, 03/09||Static semantics||Class notes|
|10||03/21, 03/23||Type Safety||Class notes|
|11||03/28, 03/30||Test II||Class notes|
|12||04/04, 04/06||Algebraic data types||Class notes|
|13||04/11, 04/13||Side effects||5.2, 7.2-7.3|
|14||04/18, 04/20||Side effects||Class notes|
|15||04/25, 04/27||Review||Class notes|
|Final||05/02||Final Exam, 3-5pm||All tests are cumulative|