In September, 2004, I posted a query to the Types list asking people to name the five most important papers ever written in the area of programming languages. This page collects the responses I received. (A few are missing because I am still tracking down bibliographic information.)

Many thanks to Frank Atanassow, David Benson, Nick Benton, Karl Crary, Olivier Danvy, Mariangiola Dezani, Dan Friedman, Alwyn Goodloe, Pieter Hartel, Michael Hicks, Robert Irwin, Luis Lamb, Rod Moten, Rishiyur Nikhil, Tobias Nipkow, Jens Palsberg, and John Reynolds for contributing.

Additional suggestions are welcome. (Bibtex format preferred!)

-- BCP

The greatest of the great (mentioned by many people):

C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580 and 583, October 1969. [bib]

Peter J. Landin. The next 700 programming languages. Communications of the ACM, 9(3):157-166, March 1966. [bib]

Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, August 1978. [bib]

Gordon Plotkin. Call-by-name, call-by-value, and the λ-calculus. Theoretical Computer Science, 1:125-159, 1975. [bib]

John C. Reynolds. Towards a theory of type structure. In Colloque sur la Programmation, Paris, France, volume 19 of Lecture Notes in Computer Science, pages 408-425. Springer-Verlag, 1974. [bib]

Pretty great works (mentioned by multiple people):

Luis Damas and Robin Milner. Principal type schemes for functional programs. In ACM Symposium on Principles of Programming Languages (POPL), Albuquerque, New Mexico, pages 207-212, 1982. [bib]

Edsger W. Dijkstra. Recursive programming. In Saul Rosen, editor, Programming Systems and Languages, chapter 3C, pages 221-227. McGraw-Hill, New York, 1960. [bib]

Edsger W. Dijkstra. Go to statement considered harmful. 11(3):147-148, March 1968. [bib]

William A. Howard. The formulas-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479-490. Academic Press, 1980. Reprint of 1969 article. [bib]

Robert Kowalski. Predicate logic as programming language. In IFIP Congress, pages 569-574, 1974. Reprinted in Computers for Artificial Intelligence Applications, (eds. Wah, B. and Li, G.-J.), IEEE Computer Society Press, Los Angeles, 1986, pp. 68-73. [bib]

Peter J. Landin. The mechanical evaluation of expressions. Computer Journal, 6(4):308-320, January 1964. [bib]

John McCarthy. Recursive functions of symbolic expressions and their computation by machine, part I. Communications of the ACM, 3(4):184-195, April 1960. [bib]

Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System-F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):527-568, May 1999. [bib]

George C. Necula. Proof-carrying code. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France, pages 106-119, January 1997. [bib]

Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223-255, 1977. [bib]

Gordon D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981. [bib]

A great number of great works (mentioned at least once):

C. Boehm and G. Jacopini. Flow diagrams, Turing machines, and languages with only two formation rules. Communications of the ACM, 9(5):366-371, 1966. [bib]

Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56-68, 1940. [bib]

Alonzo Church. The Calculi of Lambda Conversion. Princeton University Press, 1941. [bib]

Haskell B. Curry and Robert Feys. Combinatory Logic, volume 1. North Holland, 1958. Second edition, 1968. [bib]

Robert W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19-32, Providence, Rhode Island, 1967. American Mathematical Society. [bib]

Michael J. Gordon, Robin Milner, F. Lockwood Morris, Malcolm Newey, and Christopher P. Wadsworth. A metalanguage for interactive proof in LCF. Internal Report CSR-16-77, University of Edinburgh, Edinburgh, Scotland, September 1977. [bib]

C. A. R. Hoare. Proof of a program: FIND. Communications of the ACM, 14(1):39-45, January 1971. [bib]

G. Kahn. The semantics of a simple language for parallel programming. In J. L. Rosenfeld, editor, Information processing, pages 471-475, Stockholm, Sweden, Aug 1974. North Holland, Amsterdam. [bib]

Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980. [bib]

Peter Naur et al. Revised report on the algorithmic language ALGOL 60. Communications of the ACM, 6(1):1-17, January 1963. [bib]

John C. Reynolds. Types, abstraction, and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, Paris, France, pages 513-523. Elsevier, 1983. [bib]

John C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363-397, 1998. Reprinted from the proceedings of the 25th ACM National Conference (1972), with a foreword. [bib]

Dana Scott. Continuous lattices. In F. W. Lawvere, editor, Toposes, Algebraic Geometry, and Logic, number 274 in Lecture Notes in Mathematics, pages 97-136. Springer-Verlag, 1972. [bib]

Dana S. Scott. Outline of a mathematical theory of computation. Technical Monograph PRG-2, Oxford University Computing Laboratory, Oxford, England, November 1970. [bib]

D. A. Turner. A new implementation technique for applicative languages. Software - Practice and Experience, 9(1):31-49, Jan 1979. [bib]

N. Wirth. The programming language Pascal (revised report). Technical report 5, Dept. Informatik, Inst. Für Computersysteme, ETH Zürich, Zürich, Switzerland, Jul 1973. [bib]

Niklaus Wirth and C. A. R. Hoare. A contribution to the development of ALGOL. Communications of the ACM, 9(6):413-432, June 1966. [bib]