This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.

What a program means

A subject the papers are about. The loosest grouping, and the one to reach for last.

Giving a program a meaning that is not whatever the implementation does. Each does it by translating the program into something already understood -- a function, a logic, a machine that is only rules, an algebra, a type -- and what they disagree about is which of those may be assumed.

Do not read this set in year order. Two of its most influential members are dated by publication rather than composition, and sorting by year puts them decades out of place. Strachey's *Fundamental Concepts in Programming Languages* is dated 2000 and is a course of lectures given at Copenhagen in **1967** -- it is where L-values and R-values are named and where parametric and ad hoc polymorphism are first distinguished, so a great deal of the vocabulary the rest of the set uses without attribution is fixed there. Plotkin's *A structural approach to operational semantics* is dated 2004 and is the Aarhus DAIMI FN-19 report of **1981**. Read as 2004 papers they look like retrospectives; they are foundations.

The approaches are all present in their original statements. Denotational: Scott, and Strachey. Operational: Plotkin, with Landin's abstract machine as the ancestor. Axiomatic: Hoare's proof of FIND, also in `the-program-and-its-proof`. Algebraic: Hagino's categorical programming language, an Edinburgh thesis of 1987 -- the set named the algebra case in its opening sentence and held no categorical account until this record was placed.

The types thread is the longest and contains a genuine three-author result. Hindley in 1969, Milner in 1978 and Damas and Milner in 1982 arrive at and complete principal type inference across thirteen years -- read together they are the clearest case in the corpus of a result assembled rather than announced. Reynolds, Cardelli and Wegner, Pierce's textbook and Wadler's propositions-as-types carry it forward; Moggi supplies effects; Liskov appears twice, the history and the behavioural-subtyping paper that named the principle.

At the edges: Backus arguing the whole framing is wrong and programming should be liberated from the von Neumann style, Ghica compiling a semantics into hardware, and Piedeleu on string diagrams as a way of drawing rather than writing the meaning.

24 references

Propositions as types
Philip Wadler (2015) · Communications of the ACM
Programming in the λ-Calculus: From Church to Scott and back
Jan Martin Jansen (2013) · The Beauty of Functional Code · Springer
Geometry of Synthesis IV: Compiling Affine Recursion into Static Hardware
Dan R. Ghica and others (2011) · Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP '11) · Association for Computing Machinery
A structural approach to operational semantics
Gordon D. Plotkin (2004) · The Journal of Logic and Algebraic Programming · Elsevier
Types and Programming Languages
Benjamin C. Pierce (2002) · MIT Press
Fundamental Concepts in Programming Languages
Christopher Strachey (2000) · Higher-Order and Symbolic Computation · Springer
A denotational approach for type-checking in object-oriented programming languages
Roberto Ierusalimschy (1993) · Computer Languages · Elsevier
A History of CLU
Barbara Liskov (1993) · MIT Laboratory for Computer Science
The formal semantics of programming languages: an introduction
Glynn Winskel (1993) · MIT Press
Notions of computation and monads
Eugenio Moggi (1991) · Information and Computation · Elsevier
Referential transparency, definiteness and unfoldability
Harald Søndergaard and others (1990) · Acta Informatica · Springer
A Categorical Programming Language
Tatsuya Hagino (1987) · University of Edinburgh
On understanding types, data abstraction, and polymorphism
Luca Cardelli and others (1985) · ACM Computing Surveys · Association for Computing Machinery
Types, Abstraction and Parametric Polymorphism
John C. Reynolds (1983) · Information Processing 83 · North-Holland
Principal type-schemes for functional programs
Luis Damas and others (1982) · Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages · Association for Computing Machinery
Can programming be liberated from the von Neumann style? A functional style and its algebra of programs
John Backus (1978) · Communications of the ACM · Association for Computing Machinery
A theory of type polymorphism in programming
Robin Milner (1978) · Journal of Computer and System Sciences · Elsevier
Towards a theory of type structure
John C. Reynolds (1974) · Programming Symposium · Springer
Types are not sets
James H. Morris (1973) · 1st ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) · Association for Computing Machinery
Proof of a Program: FIND
C. A. R. Hoare (1971) · Communications of the ACM · Association for Computing Machinery
Toward a Mathematical Semantics for Computer Languages
Dana Scott and others (1971) · Proceedings of the Symposium on Computers and Automata · Polytechnic Press
The next 700 programming languages
P. J. Landin (1966) · Communications of the ACM · Association for Computing Machinery
The Mechanical Evaluation of Expressions
P. J. Landin (1964) · The Computer Journal · Oxford University Press
Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I
John McCarthy (1960) · Communications of the ACM · Association for Computing Machinery