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.