- 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
- 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. 1983. pdf
- Per Martin-Lof. Intuitionistic Type Theory. 1980. pdf
- John Reynolds. Definitional Interpreters for Higher-Order Programming Languages. 1972. pdf
- Dana Scott and Christopher Strachey. Towards a Mathematical Semantics for Computer Languages. 1971. pdf
- Eugenio Moggi. Computational Lambda-calculus and Monads. 1989. pdf
- 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. pdf
- 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
- 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
- Jean-Yves Girard. Linear Logic. 1987. pdf
- Maurice Herlihy. Wait-Free Synchronization 1991. pdf