Required Reading: The following is a preliminary list of papers that we'll be reading. The first four are confirmed. NOTE: due to restrictions on public redistribution of copyrighted material, these papers are not posted online. Please write to me to ask for copies.

• John McCarthy. Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I. Communications of the ACM 3(4):184-195, April 1960.
• Peter J. Landin. The next 700 programming languages. Communications of the ACM 9(3):157-166, March 1966.
• Edsger Dijkstra. Go To Statement Considered Harmful. Communications of the ACM 11(3):147-148, March, 1968.
• C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM 12(10):576-580 and 583, October 1969.
• John Reynolds. Towards a theory of Type Structure. Lecture Notes in Computer Science vol. 19, pp. 408-425, 1974.
• Guy L. Steele. LAMBDA: The Ultimate Declarative. MIT Technical Report AIM-379, November 1976.
• Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences 17:348-375, August 1978.
• Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System-F to typed assembly language. ACM Transactions on Programming Languages and Systems 21(3):527-568, May 1999.