Document Open Access Logo

The Standard Model for Programming Languages: The Birth of a Mathematical Theory of Computation

Author Simone Martini

PDF
Thumbnail PDF

File

OASIcs.Gabbrielli.8.pdf
  • Filesize: 381 kB
  • 13 pages

Document Identifiers

Author Details

Simone Martini
  • Department of Computer Science and Engineering, University of Bologna, Italy
  • INRIA, Sophia-Antipolis, Valbonne, France

Funding

  • Martini, Simone: Research partially conducted while on sabbatical leave at the Collegium - Lyon Institute for Advanced Studies, 2018-2019. Partial support from French ANR project PROGRAMme.

Acknowledgements

I am happy to thank Edgar Daylight for mentioning me Strachey’s letter to the Computer Journal, and for the many critical reactions to the main thesis of this paper.

Cite As Get BibTex

Simone Martini. The Standard Model for Programming Languages: The Birth of a Mathematical Theory of Computation. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 8:1-8:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/OASIcs.Gabbrielli.8

Abstract

Despite the insight of some of the pioneers (Turing, von Neumann, Curry, Böhm), programming the early computers was a matter of fiddling with small architecture-dependent details. Only in the sixties some form of "mathematical program development" will be in the agenda of some of the most influential players of that time. A "Mathematical Theory of Computation" is the name chosen by John McCarthy for his approach, which uses a class of recursively computable functions as an (extensional) model of a class of programs. It is the beginning of that grand endeavour to present programming as a mathematical activity, and reasoning on programs as a form of mathematical logic. An important part of this process is the standard model of programming languages - the informal assumption that the meaning of programs should be understood on an abstract machine with unbounded resources, and with true arithmetic. We present some crucial moments of this story, concluding with the emergence, in the seventies, of the need of more "intensional" semantics, like the sequential algorithms on concrete data structures. The paper is a small step of a larger project - reflecting and tracing the interaction between mathematical logic and programming (languages), identifying some of the driving forces of this process.

to Maurizio Gabbrielli, on his 60th birthday

Subject Classification

ACM Subject Classification
  • Social and professional topics → History of programming languages
  • Software and its engineering → General programming languages
Keywords
  • Semantics of programming languages
  • history of programming languages
  • mathematical theory of computation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. John W. Backus. The syntax and semantics of the proposed international algebraic language of the Zurich ACM-GAMM conference. In Proceedings Int. Conf. on Information Processing, UNESCO, pages 125-132, 1959. Google Scholar
  2. John W. Backus, F. L. Bauer, J. Green, C. Katz, J. McCarthy, A. J. Perlis, H. Rutishauser, K. Samelson, B. Vauquois, J. H. Wegstein, A. van Wijngaarden, and M. Woodger. Report on the algorithmic language ALGOL 60. Commun. ACM, 3(5):299-314, 1960. Google Scholar
  3. Gérard Berry. Séquentialité de l'évaluation formelle des lambda-expressions. In B. Robinet, editor, Program Transformations, 3eme Colloque International sur la Programmation, pages 67-80, Paris, 1978. Dunod. Google Scholar
  4. Gérard Berry. Modèles complètement adéquats et stables des lambda-calculs typés. Thèse de Doctorat d'État, Université Paris VII, 1979. Google Scholar
  5. Gérard Berry and Pierre-Louis Curien. Sequential algorithms on concrete data structures. Theor. Comput. Sci., 20:265-321, 1982. Google Scholar
  6. Corrado Böhm. Calculatrices digitales. Du déchiffrage des formules logico-mathématiques par la machine même dans la conception du programme. Annali di matematica pura e applicata, IV-37(1):1-51, 1954. Google Scholar
  7. Stephen D. Brookes. Historical introduction to "Concrete Domains" by G. Kahn and Gordon D. Plotkin. Theor. Comput. Sci., 121(1&2):179-186, 1993. Google Scholar
  8. Felice Cardone. Continuity in semantic theories of programming. History and Philosophy of Logic, 26(3):242-261, 2015. Google Scholar
  9. Felice Cardone. Games, full abstraction and full completeness. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, winter 2017 edition, 2017. Google Scholar
  10. Haskell B. Curry. On the composition of programs for automatic computing. Technical Report Memorandum 10337, Naval Ordnance Laboratory, 1949. Google Scholar
  11. Edgar Daylight. Towards a historical notion of `Turing - the father of computer science'. History and Philosophy of Logic, 36(3):205-228, 2015. Google Scholar
  12. Richard A. De Millo, Richard J. Lipton, and Alan J. Perlis. Social processes and proofs of theorems and programs. Commun. ACM, 22(5):271-280, 1979. Google Scholar
  13. Liesbeth De Mol. Turing Machines. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, winter 2019 edition, 2019. Google Scholar
  14. Liesbeth De Mol, Maarten Bullynck, and Edgar G. Daylight. Less is more in the fifties. Encounters between logical minimalism and computer design during the 1950s. IEEE Annals of the History of Computing, 2018. Google Scholar
  15. Liesbeth De Mol, Martin Carlé, and Maarten Bullyinck. Haskell before Haskell: an alternative lesson in practical logics of the ENIAC. Journal of Logic and Computation, 25(4):1011-1046, 2015. Google Scholar
  16. Edsger W. Dijkstra. A simple axiomatic basis for programming language constructs. Indagationes Mathematicae, 36:1-15, 1974. Google Scholar
  17. James H. Fetzer. Program verification: The very idea. Commun. ACM, 31(9):1048-1063, 1988. Google Scholar
  18. Robert W. Floyd. Assigning meanings to programs. Mathematical aspects of computer science, 19:19-32, 1967. Google Scholar
  19. Maurizio Gabbrielli and Simone Martini. Programming Languages: Principles and Paradigms. Undergraduate Topics in Computer Science. Springer, 2010. Google Scholar
  20. Hermann Goldstine and John von Neumann. Planning and coding of problems for an electronic computing instrument. Technical Report Part II, Volume 1-3, Institute of Advanced Studies, 1947. Google Scholar
  21. Solomon W. Golomb. Mathematical models: Uses and limitations. IEEE Transactions on Reliability, R-20(3):130-131, 1971. Google Scholar
  22. Thomas Haigh. Actually, turing did not invent the computer. CACM, 57(1):36-41, 2014. Google Scholar
  23. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576-580, 1969. Google Scholar
  24. Gilles Kahn. The semantics of a simple language for parallel processing. In Jack L. Rosenfeld, editor, Information Processing 74, Proceedings of IFIP Congress, pages 471-475. North-Holland, 1974. Google Scholar
  25. Gilles Kahn and David B. MacQueen. Coroutines and networks of parallel processes. In Information Processing 77, Proceedings of IFIP Congress, pages 993-998. North Holland, 1977. Google Scholar
  26. Gilles Kahn and Gordon D. Plotkin. Concrete domains. Theor. Comput. Sci., 121(1&2):187-277, 1993. Reprint of the IRIA-LABORIA rapport 336 (1978). Google Scholar
  27. Stephen C. Kleene. Introduction to Metamathematics. Van Nostrand, New York, 1959. Google Scholar
  28. Donald E. Knuth. Robert W Floyd, in memoriam. SIGACT News, 34(4):3-13, December 2003. Google Scholar
  29. Donald E. Knuth and Luis T. Pardo. The early development of programming languages. In N. Metropolis, J. Howlett, and Gian-Carlo Rota, editors, A History of Computing in the Twentieth Century, pages 197-273. Academic Press, New York, NY, USA, 1980. Google Scholar
  30. Peter Kroes. Engineering and the dual nature of technical artefacts. Cambridge Journal of Economics, 34(1):51-62, 2010. Google Scholar
  31. Peter J. Landin. The mechanical evaluation of expressions. The Computer Journal, 6:308-320, 1964. Google Scholar
  32. Simone Martini. Several types of types in programming languages. In Fabio Gadducci and Mirko Tavosanis, editors, HAPOC 2015, number 487 in IFIP Advances in Information and Communication Technology, pages 216-227. Springer, 2016. Google Scholar
  33. Simone Martini. Types in programming languages, between modelling, abstraction, and correctness. In Arnold Beckmann, Laurent Bienvenu, and Nataša Jonoska, editors, CiE 2016: Pursuit of the Universal, volume 9709 of LNCS, pages 164-169. Springer, 2016. Google Scholar
  34. John McCarthy. Towards a mathematical science of computation. In IFIP Congress, pages 21-28, 1962. Google Scholar
  35. John McCarthy. A basis for a mathematical theory of computation. In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems, volume 35 of Studies in Logic and the Foundations of Mathematics, pages 33-70. Elsevier, 1963. A preliminary version presented at the Western Joint IRE-AIEE-ACM 1961 Computer Conference, pp. 225-238. ACM, New York, NY, USA (1961). Google Scholar
  36. Dale Miller. Reciprocal influences between proof theory and logic programming. Philosophy & Technology, 2019. URL: https://doi.org/10.1007/s13347-019-00370-x.
  37. Robin Milner. Processes: a mathematical model of computing agents. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73, number 80 in Studies in the Logic and the Foundations of Mathematics, pages 157-174, Amsterdam, 1975. North-Holland. Google Scholar
  38. Robin Milner. A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17(3):348-375, 1978. Google Scholar
  39. Francis Lockwood Morris and Cliff B. Jones. An early program proof by Alan Turing. Annals of the History of Computing, 6:139-143, 1984. Google Scholar
  40. James H. Morris. Lambda-calculus models of programming languages. PhD thesis, MIT, 1968. Google Scholar
  41. Allen Newell, Alan J. Perlis, and Herbert A. Simon. Computer science. Science, 157(3795):1373-1374, 1967. Google Scholar
  42. David Nofre, Mark Priestley, and Gerard Alberts. When technology became language: The origins of the linguistic conception of computer programming, 1950-1960. Technology and Culture, 55:40-75, 2014. Google Scholar
  43. Gordon D. Plotkin. LCF considered as a programming language. Theor. Comput. Sci., 5(3):223-255, 1977. Google Scholar
  44. Willard Van Orman Quine. Word and Object. MIT Press, 1960. Google Scholar
  45. B. Randell. On Alan Turing and the origins of digital computers. Machine Intelligence, pages 3-20, 1972. Google Scholar
  46. Hartley Rogers. Theory of Recursive Functions and Effective Computability. McGraw Hill, New York, 1967. Google Scholar
  47. Dana Scott. Outline of a mathematical theory of computation. In Proc. Fourth Annual Princeton Conference on Information Sciences and Systems, pages 169-76, Also Tech. Mono. PRG-2, Programming Research Group, University of Oxford., 1970. Google Scholar
  48. Joseph E. Stoy. Denotational semantics: The Scott-Strachey approach to programming language theory. MIT Press, 1977. Google Scholar
  49. Christopher Strachey. An impossible program. The Computer Journal, 7(4):313, 1965. Google Scholar
  50. Christopher Strachey. Towards a formal semantics. In T.B. Jr. Steel, editor, Formal Language Description Languages for Computer Programming, pages 198-220. North-Holland, 1966. Google Scholar
  51. Christopher Strachey. Fundamental concepts in programming languages. International Summer School in Computer Programming; Copenhagen. Reprinted in Higher-Order and Symbolic Computation, 13, 11-49, 2000, August 1967. Google Scholar
  52. Christopher Strachey. The varieties of programming language. Technical Report PRG-10, Oxford University Computing Laboratory, 1973. Google Scholar
  53. Alan M. Turing. Lecture to L.M.S. Feb. 20 1947. In Turing archive, AMT/B/1, 1947. Google Scholar
  54. Alan M. Turing. Checking a large routine. In Report of a Conference on High Speed Automatic Calculating Machines, pages 70-72. University Mathematical Laboratory, Cambridge, 1949. Google Scholar
  55. Raymond Turner. Programming languages as technical artefacts. Philosophy and Technology, 27(3):377-397, 2014. Google Scholar
  56. Raymond Turner. Computational Artifacts. Springer, 2018. Google Scholar
  57. Raymond Turner and Nicola Angius. The philosophy of computer science. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy (Winter 2014 Edition). Stanford University, 2017. URL: http://plato.stanford.edu/archives/win2014/entries/computer-science.
  58. John von Neumann. Rigorous theories of control and information. Published in Theory of Self-Reproducing Automata, A. W. Burks (Ed.), University of Illinois Press, 1966, pages 42-56, 1949. Google Scholar
  59. Glyn Winskell. Events in Computation. PhD thesis, University of Edinburgh, 1981. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact