Classic Papers in Programming Languages and Logic

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.