J. McCarthy, “Towards a
mathematical science of computation,” Proceedings of the
Information Processing Cong. 62, North-Holland, Munich, West Germany,
pp. 21-28, August, 1962.
Relevance: a seminal paper in the history of formal
operational semantics
The pdf linked above is dated 1996, but the original paper was written in
1962. In a brief preface (found on the
“Towards a Mathematical Science of Computation was given at the congress IFIP-62 and published in the proceedings of that conference. It extends the results of A Basis for a Mathematical Theory of Computation which was first given in 1961.”
In the 1962 paper (page 19) he wrote
“The semantic description of the language must tell what the programs mean. The meaning of a program is its effect on the state vector in the case of a machine independent language, and its effect on the contents of memory in the case of a machine language program.”
He goes on to sketch the approach to operational semantics used most often in ACL2 and its predecessors. See page 22.