Class schedule

Lecture 1
Introduction TAPL, Chapters 1, 2.
Lectures 2-3
Ocaml Text: There are several online OCaml books and tutorials.
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..
Lecture 12
Memory and References TAPL, Chapter 13.
Lecture 13
Subtyping TAPL, Chapters 15, 17.
Lecture 14
Recursive types TAPL, Chapter 20.
Reading Assignment: P. Wadler, 2000. Proofs are Programs: 19th Century Logic and 21st Century Computing. (pdf)
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 exam  
Lecture 18
Alias analysis: Unification Reading Assignment: Points-to analysis in almost linear time
Lecture 19
Reading Assignment: 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
Hoare Logic LICS:MRAS, Chapter 4.
A. Hoare, An axiomatic basis for computer programming.
Project due
Final exam Final project report due