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 Ley-Wild)
-
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 Ashley-Rollman)
-
C. A. R. Hoare. Communicating Sequential Processes. 1978.
(pdf)
-
October 7 (Chris Martens)
-
Per Martin-Lof. On the Meanings of the Logical Constants and the Justifications of the Logical Laws. (The Siena Lectures) 1983.
(pdf)
-
(Optional) Per Martin-Lof. Intuitionistic Type Theory. (The Padova Lectures) 1980.
(pdf)
-
October 12 (Miguel Silva)
-
John Reynolds. Definitional Interpreters for Higher-Order 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 Lambda-calculus 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 Formulae-as-Types Notion of Construction. 1969, 1980.
(pdf)
-
November 2 (Arbob Ahmad)
-
John Reynolds. Toward a Theory of Type Structure. 1974.
(pdf)
-
November 4 (Michael Ashley-Rollman)
-
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.
Higher-Order Modules and the Phase Distinction. 1989.
(pdf)
-
November 23 (Rob Simmons)
-
Luis Damas and Robin Milner.
Principal Type-Schemes for Functional Programs. 1982.
(pdf)
-
November 30 (Miguel Silva)
-
Dana Scott.
A Type-Theoretical Alternative to ISWIM, CUCH, OWHY. 1969, 1993.
(pdf)
-
December 2 (Ruy Ley-Wild)
-
Jean-Yves Girard.
Linear Logic. 1987.
(pdf)
Note: this paper is very long. Be sure at least to skim the whole thing.