Class schedule

Lecture 1
Introduction TAPL, Chapters 1, 2.
Lectures 2-3
Ocaml Text: There are several online OCaml books and tutorials.
Reading: Patterson's Research Talk
Lecture 4
Simple arithmetic: syntax, semantics, evaluation TAPL, Chapters 3, 4.
Homework 1 out: Ocaml functions.
Homework 1 due: 15 Oct., 23:59.
Lecture 5
Untyped lambda calculus: syntax, basic examples TAPL, Chapter 5.
Reading Assignment: Landin, P. J. (1966). The next 700 programming languages. Communications of the ACM, 9(3), 157-166. Due Oct 16.
Lecture 6
Untyped lambda calculus: semantics and implementation TAPL, Chapters 6, 7.
Lecture 7
Untyped lambda calculus: Writing the interpreter Examples, guideline, exercises
Lecture 8
Types and type rules TAPL, Chapter 8.
Lecture 9
Simply typed lambda calculus: The function type TAPL, Chapter 9.
Reading Assignment: Edsger W. Dijkstra. Recursive programming. In Saul Rosen, editor, Programming Systems and Languages, chapter 3C, pages 221-227. McGraw-Hill, New York, 1960.
AND Edsger W. Dijkstra. Go to statement considered harmful. 11(3):147-148, March 1968.
Due Oct 23.
Homework 2 out: A lambda calculus interpreter Due: 06 Nov..
Lecture 10
Simply typed lambda calculus: Typechecking TAPL, Chapter 10.
Lecture 11
Adding more types: unit, tuples, pairs, sums, variants, lists, etc TAPL, Chapter 11.
Homework 3 out: Write the typechecker for the function, bool, unit types Due: 15 Nov..
Reading Assignment: P. Wadler, 2000. Proofs are Programs: 19th Century Logic and 21st Century Computing. (pdf)
Midterm
in class
Lecture 12
Memory and References TAPL, Chapter 13.
Lecture 13
Subtyping TAPL, Chapters 15, 17.
Lecture 14
Recursive types TAPL, Chapter 20.
Lecture 15
Curry-Howard isomorphism  
Lecture 16, 17
The control-flow graph PPA, Chapters 2, 3.
Reading Assignment: Necula, George C. "Proof-carrying code." Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 1997.
Midterm
Midterm exam  
Lecture 18
Alias analysis: Unification Reading Assignment: Points-to analysis in almost linear time
Lecture 19
Alias analysis: Subtyping Reading Assignment: Program Analysis and Specialization for the C Programming Language
Pointer analysis: haven't we solved this problem yet?, Michael Hind
Lectures 20-21
Hoare Logic LICS:MRAS, Chapter 4.
A. Hoare, An axiomatic basis for computer programming.
Final
Final exam Final project report due