Final grades are posted in Canvas.
Assignment I, handed out on 1/9 and due on 1/23
Assignment II, handed out on 1/25 and due on 2/6
Assignment III, handed out on 2/20 and due on 2/27
Assignment IV, handed out on 2/27 and due on 3/20
Assignment V, handed out on 3/20 and due on 4/10
Test II (given on 3/27)
Assignment VI, handed out on 4/10 and due on 4/24
Test III (given on 5/1)
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/09, 01/11||Introduction; ML basics; Polymorphism||1-3.1, 5.3|
|2||01/18||Functions; Patterns||3.2-3.6.3, 4.1-4.2|
|3||01/23, 01/25||Functions||5.1, 5.4-5.6|
|4||01/30, 02/01||Datatypes; Deductive Systems||6.1-6.3|
|5||02/06, 02/08||Deductive systems; Syntax||Class notes|
|6||02/13, 02/15||Test I||Class notes|
|7||02/20, 02/22||Syntax; Dynamic semantics||Class notes|
|8||02/27, 03/01||Lambda calculus||Class notes|
|9||03/06, 03/08||Lambda calculus; Static semantics||Class notes|
|10||03/20, 03/22||Type safety||Class notes|
|11||03/27, 03/29||Test II||Class notes|
|12||04/03, 04/05||Algebraic data types||Class notes|
|13||04/10, 04/12||Recursive types; Side effects||5.2, 7.2-7.3|
|14||04/17, 04/19||Side effects||Class notes|
|15||04/24, 04/26||Side effects||Class notes|
|Final||05/01||Test III (Final Exam), 3-5pm||All tests are cumulative|