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: 14 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 before class.
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 before class.
Homework 2 out: A lambda calculus interpreter Due: 29 Oct..
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: 13 Nov..
Reading Assignment: P. Wadler, 2000. Proofs are Programs: 19th Century Logic and 21st Century Computing. (pdf)
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
Lectures 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.
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