This page is copied from Classic Papers in Programming Languages and Logic
- 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)
- 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.
- P. J. Landin. The Next 700 Programming Languages. 1966.(pdf)
- Gerhard Gentzen. Investigations into Logical Deduction. 1935.(pdf)
- P. J. Landin. The Mechanical Evaluation of Expressions. 1964.(pdf)
- John McCarthy. Recursive Functions of Symbolic Expressions and Their Computation By Machine, Part I. 1960.(pdf)
- Gordon Plotkin. A Structural Approach to Operational Semantics. 1981.(pdf)
- C. A. R. Hoare. Communicating Sequential Processes. 1978.(pdf)
- 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)
- John Reynolds. Definitional Interpreters for Higher-Order Programming Languages. 1972.(ps)
- Dana Scott and Christopher Strachey. Towards a Mathematical Semantics for Computer Languages. 1971.(pdf, now with page 20)
- Eugenio Moggi. Computational Lambda-calculus and Monads. 1989.(pdf)
- (Optional) Eugenio Moggi. Notions of Computation and Monads. 1991.(pdf)
- John Backus. Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs. 1978.(pdf)
- John Reynolds. The Essence of Algol. 1981.(ps)
- W. A. Howard. The Formulae-as-Types Notion of Construction. 1969, 1980.(pdf)
- John Reynolds. Toward a Theory of Type Structure. 1974.(pdf)
- Chetan Murthy. An Evaluation Semantics for Classical Proofs. 1991.(pdf)
- John Reynolds. Types, Abstraction, and Parametric Polymorphism. 1983.(pdf)
- (Optional) Christoper Strachey. Fundamental Concepts in Programming Languages. 1967.(pdf)
- John Mitchell and Gordon Plotkin. Abstract Types have Existential Types. 1985, 1988.(pdf)
- David B. MacQueen. Using Dependent Types to Express Modular Structure. 1986.(pdf)
- Robert Harper, John C. Mitchell, and Eugenio Moggi.Higher-Order Modules and the Phase Distinction. 1989.(pdf)
- Luis Damas and Robin Milner.Principal Type-Schemes for Functional Programs. 1982.(pdf)
- Dana Scott.A Type-Theoretical Alternative to ISWIM, CUCH, OWHY. 1969, 1993.(pdf)
- Jean-Yves Girard.Linear Logic. 1987.(pdf)