Classic Papers in Programming Languages and Logic
The class meets Monday and Wednesday at 3pm in GHC 4101.
Reading list

September 9 (Karl Crary)

C. A. R. Hoare. An Axiomatic Basis for Computer Programming. 1969.
(pdf)

Edsger W. Dijkstra. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. 1975.
(pdf)

(Optional)
C. A. R. Hoare. Proof of a Program: FIND. 1971.
(pdf)

September 14 (Rob Simmons)

Alonzo Church and J. B. Rosser. Some Properties of Conversion. 1936.
(pdf)
Note: rule I is alpha conversion, rule II is beta reduction, and rule
III is beta expansion.

September 16 (Ruy LeyWild)

P. J. Landin. The Next 700 Programming Languages. 1966.
(pdf)

September 21 (William Lovas)

Gerhard Gentzen. Investigations into Logical Deduction. 1935.
(pdf)

September 23 (Anand Subramanian)

P. J. Landin. The Mechanical Evaluation of Expressions. 1964.
(pdf)

September 28 (Luke Zarko)

John McCarthy. Recursive Functions of Symbolic Expressions and Their Computation By Machine, Part I. 1960.
(pdf)

September 30 (Arbob Ahmad)

Gordon Plotkin. A Structural Approach to Operational Semantics. 1981.
(pdf)
Note: this paper is very long. Be sure at least to skim the whole thing.

October 5 (Michael AshleyRollman)

C. A. R. Hoare. Communicating Sequential Processes. 1978.
(pdf)

October 7 (Chris Martens)

Per MartinLof. On the Meanings of the Logical Constants and the Justifications of the Logical Laws. (The Siena Lectures) 1983.
(pdf)

(Optional) Per MartinLof. Intuitionistic Type Theory. (The Padova Lectures) 1980.
(pdf)

October 12 (Miguel Silva)

John Reynolds. Definitional Interpreters for HigherOrder Programming Languages. 1972.
(ps)

October 14 (Rob Simmons)

Dana Scott and Christopher Strachey. Towards a Mathematical Semantics for Computer Languages. 1971.
(pdf, now with page 20)

October 19 (Rob Arnold)

Eugenio Moggi. Computational Lambdacalculus and Monads. 1989.
(pdf)

(Optional) Eugenio Moggi. Notions of Computation and Monads. 1991.
(pdf)

October 21 (William Lovas)

John Backus. Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs. 1978.
(pdf)

October 26 (Anand Subramanian)

John Reynolds. The Essence of Algol. 1981.
(ps)

October 28 (Chris Martens)

W. A. Howard. The FormulaeasTypes Notion of Construction. 1969, 1980.
(pdf)

November 2 (Arbob Ahmad)

John Reynolds. Toward a Theory of Type Structure. 1974.
(pdf)

November 4 (Michael AshleyRollman)

Chetan Murthy. An Evaluation Semantics for Classical Proofs. 1991.
(pdf)

November 9 (Rob Arnold)

John Reynolds. Types, Abstraction, and Parametric Polymorphism. 1983.
(pdf)

(Optional) Christoper Strachey. Fundamental Concepts in Programming Languages. 1967.
(pdf)

November 11 (Henry DeYoung)

John Mitchell and Gordon Plotkin. Abstract Types have Existential Types. 1985, 1988.
(pdf)

November 16 (Luke Zarko)

David B. MacQueen. Using Dependent Types to Express Modular Structure. 1986.
(pdf)

November 18 (Henry DeYoung)

Robert Harper, John C. Mitchell, and Eugenio Moggi.
HigherOrder Modules and the Phase Distinction. 1989.
(pdf)

November 23 (Rob Simmons)

Luis Damas and Robin Milner.
Principal TypeSchemes for Functional Programs. 1982.
(pdf)

November 30 (Miguel Silva)

Dana Scott.
A TypeTheoretical Alternative to ISWIM, CUCH, OWHY. 1969, 1993.
(pdf)

December 2 (Ruy LeyWild)

JeanYves Girard.
Linear Logic. 1987.
(pdf)
Note: this paper is very long. Be sure at least to skim the whole thing.