• Top
    • Documentation
      • Xdoc
      • ACL2-doc
      • Recursion-and-induction
      • Loop$-primer
      • Operational-semantics
        • Operational-semantics-3__annotated-bibliography
          • Bib::bhmy89
          • Bib::liu06
          • Bib::bm96
          • Bib::plotkin04b
          • Bib::bgm90
          • Bib::hkms17
          • Bib::bkm96
          • Bib::moore15
          • Bib::bh99
          • Bib::wilding93
          • Bib::plotkin04a
          • Bib::moore03b
          • Bib::mp02
          • Bib::moore19
          • Bib::manolios00
          • Bib::flatau92
          • Bib::hb92
          • Bib::bm05
          • Bib::goel16
          • Bib::bm73
          • Bib::ghk17
          • Bib::wilding92
          • Bib::moore17
          • Bib::moore96
          • Bib::ghkg14
          • Bib::yu92
          • Bib::hunt85
          • Bib::boh03
          • Bib::mmrv06
          • Bib::bm80
          • Bib::bh97
          • Bib::moore99b
          • Bib::moore14
          • Bib::rm04
          • Bib::by96
          • Bib::sawada00
          • Bib::mccarthy62
            • Bib::bm79
            • Bib::moore99a
            • Bib::sh98
            • Bib::rhmm07
            • Bib::kmm00a
            • Bib::ghk13
            • Bib::moore03a
            • Bib::hk12
            • Bib::mp67
            • Bib::young88
            • Bib::bm97
            • Bib::moore73
            • Bib::kmm00b
            • Bib::bevier87
          • Operational-semantics-1__simple-example
          • Operational-semantics-2__other-examples
          • Operational-semantics-5__history-etc
          • Operational-semantics-4__how-to-find-things
        • Pointers
        • Doc
        • Documentation-copyright
        • Course-materials
        • Publications
        • Args
        • ACL2-doc-summary
        • Finding-documentation
        • Broken-link
        • Doc-terminal-test-2
        • Doc-terminal-test-1
      • Books
      • Boolean-reasoning
      • Projects
      • Debugging
      • Std
      • Community
      • Proof-automation
      • ACL2
      • Macro-libraries
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Operational-semantics-3__annotated-bibliography

    Bib::mccarthy62

    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 .html file at the same site as the link above) to the 1996 paper McCarthy wrote:

    “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.