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: 16 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
Reading Assignment: P. Wadler, 2000. Proofs are Programs: 19th Century Logic and 21st Century Computing. (pdf)
Homework 2 out: Interpreter.
Due: 30 Oct., 23:59.
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.
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: C. A. R. Hoare. Communicating Sequential Processes. 1978.
Midterm
 in class
Lecture 12
 Memory and References TAPL, Chapter 13.
Lecture 13
 Subtyping TAPL, Chapters 15, 17.
Reading Assignment: Luis Damas and Robin Milner. Principal Type-Schemes for Functional Programs. 1982.
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