Class schedule

Lecture 1
23 Sept.		 Introduction TAPL, Chapters 1, 2.
Lectures 2-3
28, 30 Sept.		 Ocaml Text: There are several online OCaml books and tutorials.
Lecture 4
5, 7, 12 Oct.		 Simple arithmetic: syntax, semantics, evaluation TAPL, Chapters 3, 4.
Homework 1 out: Ocaml functions.
Homework 1 due: 18 Oct., 23:59.
Lecture 5
14, 19 Oct.		 Untyped lambda calculus: syntax, basic examples TAPL, Chapter 5.
Lecture 6
21, 26 Oct.		 Untyped lambda calculus: semantics and implementation TAPL, Chapters 6, 7.
Lecture 7
02 Nov.		 Untyped lambda calculus: Writing the interpreter Examples, guideline, exercises
Homework 2 out: A lambda calculus interpreter
Lecture 8
04 Nov.		 Types and type rules TAPL, Chapter 8.
Lecture 9
09 Nov.		 Simply typed lambda calculus: The function type TAPL, Chapter 9.
Homework 2 due: 16 Nov., 23:59.
Lecture 10
16 Nov.		 Simply typed lambda calculus: Typechecking TAPL, Chapter 10.
Homework 3 out: Write the typechecker for the function, bool, unit types
Homework 3 due: 08 Dec., 23:59.
Lecture 11
18 Nov.		 Adding more types: unit, tuples, pairs, sums, variants, lists, etc TAPL, Chapter 11.
Lecture 12
20 Nov.		 Memory and References TAPL, Chapter 13.
Lecture 13
23 Nov.		 Subtyping TAPL, Chapters 15, 17.
Lecture 14
25 Nov.		 Recursive types TAPL, Chapter 20.
Lecture 15
30 Nov.		 Curry-Howard isomorphism  
Midterm
02 Dec.		 Midterm exam  
Lecture 16, 17
07 Dec.		 The control-flow graph PPA, Chapters 2, 3.
Lecture 18
09 Dec.		 Alias analysis: Unification Points-to analysis in almost linear time
Lecture 19
14 Dec.		 Alias analysis: Subtyping Program Analysis and Specialization for the C Programming Language
Pointer analysis: haven't we solved this problem yet?, Michael Hind
Lectures 20-21
16 Dec.		 Hoare Logic LICS:MRAS, Chapter 4.
A. Hoare, An axiomatic basis for computer programming.
Project due
Final
?? Jan.		 Final exam Final project report due