Advertisement

Challenges for Formal Semantic Description: Responses from the Main Approaches

  • Cliff B. JonesEmail author
  • Troy K. Astarte
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11174)

Abstract

Although there are thousands of programming languages, most of them share common features. This paper reviews some key underlying language concepts and the challenges they present to the task of formally describing language semantics. The responses to these challenges in operational, axiomatic and denotational approaches to semantic description are reviewed. There are interesting overlaps between these responses; similarities are exposed even where accidental notational conventions disguise them so that essential differences can be pinpointed. Depending on the objectives of writing a formal semantic description of a language, one or other approach might be considered the best choice. An argument is made for increasing the use of formal semantics in language design and here it is suggested that the operational approach is the most viable for a complete language description.

Notes

Acknowledgements

The authors are extremely grateful to Mike Dodds, Shmuel Tyszberowicz and Ian Hayes for constructive and detailed comments on drafts of this paper. Some of the material was also presented at HaPoC-2017 in Oxford and useful comments were made by participants. Funding for the authors’ research comes from UK EPSRC both as a PhD studentship and the Strata Platform grant.

References

  1. [Abr10]
    Abrial, J.-R.: The Event-B Book. Cambridge University Press, Cambridge (2010)zbMATHGoogle Scholar
  2. [ACJ72]
    Allen, C.D., Chapman, D.N., Jones, C.B.: A formal definition of ALGOL 60. Technical report 12.105, IBM Laboratory Hursley, August 1972Google Scholar
  3. [Acz82]
    Aczel, P.: A note on program verification. Manuscript (private communication), Manchester, January 1982Google Scholar
  4. [Acz83]
    Aczel, P.H.G.: On an inference rule for parallel composition. Private communication (1983)Google Scholar
  5. [AGM92]
    Abramsky, S., Gabbay, D.M., Maibaum, S.E. (eds.) Handbook of Logic in Computer Science: Background: Computational Structures, vol. 2. Oxford University Press Inc., New York (1992)Google Scholar
  6. [AJ18]
    Astarte, T.K., Jones, C.B.: Formal semantics of ALGOL 60: four descriptions in their historical context. In: De Mol, L., Primiero, G. (eds.) Reflections on Programming Systems - Historical and Philosophical Aspects, pp. 71–141. Springer Philosophical Studies Series (2018, in press)Google Scholar
  7. [Ame89]
    America, P.H.M.: The practical importance of formal semantics. In: de Bakker, J.W. (ed.) 25 jaar semantiek. CWI (1989)Google Scholar
  8. [ANS76]
    ANSI: Programming language PL/I. Technical report X3.53-1976, American National Standard (1976)Google Scholar
  9. [Apt81]
    Apt, K.R.: Ten years of Hoare’s logic: a survey–part I. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981)CrossRefGoogle Scholar
  10. [Apt84]
    Apt, K.R.: Ten years of Hoare’s logic: a survey - part II: nondeterminism. Theor. Comput. Sci. 28, 83–109 (1984)CrossRefGoogle Scholar
  11. [AR92]
    America, P., Rutten, J.: A layered semantics for a parallel object-oriented language. Form. Asp. Comput. 4(4), 376–408 (1992)CrossRefGoogle Scholar
  12. [Ast19]
    Astarte, T.K.: Formalising meaning: a history of programming language semantics. Ph.D. thesis, Newcastle University (2019, forthcoming)Google Scholar
  13. [BBG+60]
    Backus, J.W., et al.: Report on the algorithmic language ALGOL 60. Numerische Mathematik 2(1), 106–136 (1960)MathSciNetCrossRefGoogle Scholar
  14. [BBH+74]
    Bekič, H., Bjørner, D., Henhapl, W., Jones, C.B., Lucas, P.: A formal definition of a PL/I subset. Technical report 25.139, IBM Laboratory Vienna, December 1974Google Scholar
  15. [BG80]
    Burstall, R.M., Goguen, J.A.: The semantics of clear, a specification language. In: Bjøorner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 292–332. Springer, Heidelberg (1980).  https://doi.org/10.1007/3-540-10007-5_41CrossRefGoogle Scholar
  16. [BIJW75]
    Bekič, H., Izbicki, H., Jones, C.B., Weissenböck, F.: Some experiments with using a formal language definition in compiler development. Laboratory note LN 25.3.107, IBM Laboratory Vienna, December 1975Google Scholar
  17. [BJQ2000]
    Bowen, J.P., Jifeng, H., Qiwen, X.: An animatable operational semantics of the Verilog hardware description language. In: Formal Engineering Methods, pp. 199–207. IEEE (2000 )Google Scholar
  18. [BK84]
    Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control 60(1–3), 109–137 (1984)MathSciNetCrossRefGoogle Scholar
  19. [BO80]
    Bjørner, D., Nest, O.N. (eds.): Towards a Formal Description of Ada. LNCS, vol. 98. Springer, Heidelberg (1980).  https://doi.org/10.1007/3-540-10283-3CrossRefzbMATHGoogle Scholar
  20. [BO16]
    Brookes, S., O’Hearn, P.W.: Concurrent separation logic. ACM SIGLOG News 3(3), 47–65 (2016)Google Scholar
  21. [Bur66]
    Burstall, R.M.: Semantics of assignment. Mach. Intell. 2, 3–20 (1966)zbMATHGoogle Scholar
  22. [BvW98]
    Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (1998).  https://doi.org/10.1007/978-1-4612-1674-2CrossRefzbMATHGoogle Scholar
  23. [CG90]
    Carré, B., Garnsworthy, J.: Spark–an annotated Ada subset for safety-critical programming. In: Proceedings of the Conference on TRI-ADA 1990, TRI-Ada 1990, pp. 392–402. ACM (1990)Google Scholar
  24. [CH72]
    Clint, M., Hoare, C.A.R.: Program proving: jumps and functions. Acta Informatica 1(3), 214–224 (1972)CrossRefGoogle Scholar
  25. [CHM16]
    Colvin, R.J., Hayes, I.J., Meinicke, L.A.: Designing a semantic model for a wide-spectrum language with concurrency. Form. Asp. Comput. 29(5), 1–22 (2016)MathSciNetzbMATHGoogle Scholar
  26. [CJ06]
    Coleman, J.W., Jones, C.B.: Guaranteeing the soundness of rely/guarantee rules. Technical report CS-TR-955, School of Computing Science, University of Newcastle, March 2006Google Scholar
  27. [Col08]
    Coleman, J.W.: Constructing a tractable reasoning framework upon a fine-grained structural operational semantics. Ph.D. thesis, Newcastle University, January 2008Google Scholar
  28. [Dat82]
    Date, C.J.: A formal definition of the relational model. ACM SIGMOD Rec. 13(1), 18–29 (1982)CrossRefGoogle Scholar
  29. [dB91]
    Boer, F.S.: A proof system for the language POOL. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.) REX 1990. LNCS, vol. 489, pp. 124–150. Springer, Heidelberg (1991).  https://doi.org/10.1007/BFb0019442CrossRefGoogle Scholar
  30. [dBDBZ80]
    de Bakker, J.W., De Bruin, A., Zucker, J.: Mathematical Theory of Program Correctness, vol. 980. Prentice-Hall International, London (1980)Google Scholar
  31. [Dij68]
    Dijkstra, E.W.: Go to statement considered harmful. Commun. ACM 11(3), 147–148 (1968)CrossRefGoogle Scholar
  32. [Dij76]
    Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)zbMATHGoogle Scholar
  33. [DMN68]
    Dahl, O.-J., Myhrhaug, B., Nygaard, K.: SIMULA 67 common base language. Technical report S-2, Norwegian Computing Center, Oslo (1968)Google Scholar
  34. [Don76]
    Donahue, J.E.: Complementary Definitions of Programming Language Semantics. LNCS, vol. 42. Springer, Heidelberg (1976).  https://doi.org/10.1007/BFb0025364CrossRefzbMATHGoogle Scholar
  35. [dR01]
    de Roever, W.P.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  36. [DS90]
    Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, New York (1990).  https://doi.org/10.1007/978-1-4612-3228-5CrossRefzbMATHGoogle Scholar
  37. [Flo67]
    Floyd, R.W.: Assigning meanings to programs. In: Proceedings of Symposium in Applied Mathematics. Mathematical Aspects of Computer Science, vol. 19, pp. 19–32. American Mathematical Society (1967)Google Scholar
  38. [Gor75]
    Gordon, M.: Operational reasoning and denotational semantics. Technical report STAN-CS-75-506, Computer Science Department, Stanford University, August 1975Google Scholar
  39. [Gor95]
    Gordon, M.: The semantic challenge of Verilog HDL. In: Proceedings of theTenth Annual IEEE Symposium on Logic in Computer Science, LICS 1995, pp. 136–145. IEEE (1995)Google Scholar
  40. [GP99]
    Gabbay, M., Pitts, A.: A new approach to abstract syntax involving binders. In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, LICS 1999. IEEE Computer Society (1999)Google Scholar
  41. [GR83]
    Goldberg, A., Robson, D.: Smalltalk-80: The Language and Its Implementation. Addison-Wesley, Boston (1983)zbMATHGoogle Scholar
  42. [Hay16]
    Hayes, I.J.: Generalised rely-guarantee concurrency: an algebraic foundation. Form. Asp. Comput. 28(6), 1057–1078 (2016)MathSciNetCrossRefGoogle Scholar
  43. [HCM+16]
    Hayes, I.J., Colvin, R.J., Meinicke, L.A., Winter, K., Velykis, A.: An algebra of synchronous atomic steps. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 352–369. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-48989-6_22CrossRefGoogle Scholar
  44. [HHJ+87]
    Hoare, C.A.R., et al.: Laws of programming. Commun. ACM 30(8), 672–687 (1987). See Corrigenda in Commun. ACM 30(9), 770MathSciNetCrossRefGoogle Scholar
  45. [HJ73]
    Hanford, K.V., Jones, C.B.: Dynamic syntax: a concept for the definition of the syntax of programming languages. In: Annual Review in Automatic Programming, vol. 7, pp. 115–140. Pergamon (1973)Google Scholar
  46. [HJ08]
    Hughes, J.R.D., Jones, C.B.: Reasoning about programs via operational semantics: requirements for a support system. Autom. Softw. Eng. 15(3–4), 299–312 (2008)CrossRefGoogle Scholar
  47. [HJC14]
    Hayes, I.J., Jones, C.B., Colvin, R.J.: Laws and semantics for rely-guarantee refinement. Technical report CS-TR-1425, Newcastle University, July 2014Google Scholar
  48. [HMRC87]
    Holt, R.C., Matthews, P.A., Rosselet, J.A., Cordy, J.R.: The Turing Programming Language: Design and Definition. Prentice-Hall Inc., Upper Saddle River (1987)Google Scholar
  49. [HMSW11]
    Hoare, C.A.R., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene Algebra and its foundations. J. Log. Algebr. Program. 80(6), 266–296 (2011)MathSciNetCrossRefGoogle Scholar
  50. [HMT87]
    Harper, R., Milner, R., Tofte, M.: The semantics of standard ML: version 1, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh (1987). Hard copyGoogle Scholar
  51. [Hoa69]
    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRefGoogle Scholar
  52. [Hoa71a]
    Hoare, C.A.R.: Procedures and parameters: an axiomatic approach. In: Engeler, E. (ed.) Symposium on Semantics of Algorithmic Languages. LNM, vol. 188, pp. 102–116. Springer, Berlin (1971)CrossRefGoogle Scholar
  53. [Hoa71b]
    Hoare, C.A.R.: Proof of a program: FIND. Commun. ACM 14(1), 39–45 (1971)CrossRefGoogle Scholar
  54. [Hoa72a]
    Hoare, C.A.R.: A note on the FOR statement. BIT 12(3), 334–341 (1972)CrossRefGoogle Scholar
  55. [Hoa72b]
    C.A.R. Hoare. Towards a theory of parallel programming. In Operating System Techniques, pages 61–71. Academic Press, 1972Google Scholar
  56. [Hoa73]
    Hoare, C.A.R: Hints on programming language design. Invited Address at SIGACT/SIGPLAN Symposium on Principles of Programming Languages, Boston, October 1973Google Scholar
  57. [Hoa85]
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)zbMATHGoogle Scholar
  58. [Hug11]
    Hughes, J.R.D.: Reasoning about programs using operational semantics and the role of a proof support tool. Ph.D. thesis, Newcastle University (2011)Google Scholar
  59. [HvS12]
    Hoare, T., van Staden, S.: In praise of algebra. Form. Asp. Comput. 24(4–6), 423–431 (2012)MathSciNetCrossRefGoogle Scholar
  60. [INM88]
    INMOS. occam 2: Reference Manual. Prentice Hall (1988)Google Scholar
  61. [Izb75]
    Izbicki, H.: On a consistency proof of a chapter of a formal definition of a PL/I subset. Technical report TR 25.142, IBM Laboratory Vienna, February 1975Google Scholar
  62. [JA16]
    Jones, C.B., Astarte, T.K.: An exegesis of four formal descriptions of ALGOL 60. Technical report CS-TR-1498 School of Computer Science, Newcastle University, September 2016. Forthcoming as a paper in the HaPoP 2016 ProceedingsGoogle Scholar
  63. [JH16]
    Jones, C.B., Hayes, I.J.: Possible values: exploring a concept for concurrency. J. Log. Algebraic Methods Program. 85, 972–984 (2016)MathSciNetCrossRefGoogle Scholar
  64. [JHC15]
    Jones, C.B., Hayes, I.J., Colvin, R.J.: Balancing expressiveness in formal approaches to concurrency. Form. Asp. Comput. 27(3), 465–497 (2015)MathSciNetCrossRefGoogle Scholar
  65. [JL71]
    Jones, C.B., Lucas, P.: Proving correctness of implementation techniques. In: Engeler, E. (ed.) Symposium on Semantics of Algorithmic Languages. LNM, vol. 188, pp. 178–211. Springer, Heidelberg (1971).  https://doi.org/10.1007/BFb0059698CrossRefGoogle Scholar
  66. [JLRW05]
    Jones, C.B., Lomet, D., Romanovsky, A., Weikum, G.: The atomic manifesto: a story in four quarks. ACM SIGMOD Rec. 34(1), 63–69 (2005)CrossRefGoogle Scholar
  67. [Jon69]
    Jones, C.B.: A proof of the correctness of some optimising techniques. Technical report LN 25.3.051, IBM Laboratory, Vienna, June 1969Google Scholar
  68. [Jon76]
    Jones, C.B.: Formal definition in compiler development. Technical report 25.145, IBM Laboratory Vienna, February 1976Google Scholar
  69. [Jon78]
    Jones, C.B.: Denotational semantics of goto: an exit formulation and its relation to continuations. In Bjørner and Jones [BJ78], pp. 278–304Google Scholar
  70. [Jon80]
    Jones, C.B.: Software Development: a Rigorous Approach. Prentice Hall International, Englewood Cliffs (1980)zbMATHGoogle Scholar
  71. [Jon81]
    Jones, C.B.: Development methods for computer programs including a notion of interference. Ph.D. thesis, Oxford University, June 1981. Printed as: Programming Research Group, Technical Monograph 25Google Scholar
  72. [Jon82]
    Jones, C.B.: More on exception mechanisms. In: Bjørner and Jones [BJ82], Chap. 5, pp. 125–140Google Scholar
  73. [Jon90]
    Jones, C.B.: Systematic Software Development using VDM, 2nd edn. Prentice Hall International, Upper Saddle River (1990)zbMATHGoogle Scholar
  74. [Jon03]
    Jones, C.B.: The early search for tractable ways of reasoning about programs. IEEE Ann. Hist. Comput. 25(2), 26–49 (2003)MathSciNetCrossRefGoogle Scholar
  75. [JP11]
    Jones, C.B., Pierce, K.G.: Elucidating concurrent algorithms via layers of abstraction and reification. Form. Asp. Comput. 23(3), 289–306 (2011)MathSciNetCrossRefGoogle Scholar
  76. [JY15]
    Jones, C.B., Yatapanage, N.: Reasoning about separation using abstraction and reification. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 3–19. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-22969-0_1CrossRefzbMATHGoogle Scholar
  77. [Kah87]
    Kahn, G.: Natural semantics. In: Brandenburg, F.J., Vidal-Naquet, G., Wirsing, M. (eds.) STACS 1987. LNCS, vol. 247, pp. 22–39. Springer, Heidelberg (1987).  https://doi.org/10.1007/BFb0039592CrossRefGoogle Scholar
  78. [KB12]
    Kloos, C.D., Breuer, P.: Formal Semantics for VHDL. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-1-4615-2237-9CrossRefzbMATHGoogle Scholar
  79. [Kin69]
    King, J.C.: A program verifier. Ph.D. thesis, Department of Computer Science, Carnegie-Mellon University (1969)Google Scholar
  80. [Knu64]
    Knuth, D.E.: Man or boy. ALGOL Bull. 17(7) (1964)Google Scholar
  81. [Knu68]
    Knuth, D.E.: Semantics of context-free languages. Theory Comput. Syst. 2(2), 127–145 (1968)MathSciNetzbMATHGoogle Scholar
  82. [Knu74]
    Knuth, D.E.: Structured programming with GO TO statements. Technical report STAN-CS-74-416, Computer Science Dept, Stanford University, May 1974CrossRefGoogle Scholar
  83. [Koz97]
    Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427–443 (1997)CrossRefGoogle Scholar
  84. [Lab66]
    Vienna Laboratory: Formal definition of PL/I (Universal Language Document No. 3). Technical report 25.071, IBM Laboratory Vienna, December 1966Google Scholar
  85. [Lan65a]
    Landin, P.J.: A correspondence between ALGOL 60 and Church’s lambda-notation: part I. Commun. ACM 8(2), 89–101 (1965)MathSciNetCrossRefGoogle Scholar
  86. [Lan65b]
    Landin, P.J.: A correspondence between ALGOL 60 and Church’s lambda-notation: part II. Commun. ACM 8(3), 158–167 (1965)MathSciNetCrossRefGoogle Scholar
  87. [Lau71]
    Lauer, P.E.: Consistent formal theories of the semantics of programming languages. Ph.D. thesis, Queen’s University of Belfast (1971). Printed as TR 25.121, IBM Lab. ViennaGoogle Scholar
  88. [LPP70]
    Luckham, D.C., Park, D.M.R., Paterson, M.S.: On formalised computer programs. J. Comput. Syst. Sci. 4(3), 220–249 (1970)MathSciNetCrossRefGoogle Scholar
  89. [Luc68]
    Lucas, P.: Two constructive realisations of the block concept and their equivalence. Technical report TR 25.085, IBM Laboratory Vienna, June 1968Google Scholar
  90. [LW69]
    Lucas, P., Walk, K.: On the formal description of PL/I. Annu. Rev. Autom. Program. 6, 105–182 (1969)CrossRefGoogle Scholar
  91. [McC63]
    McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress, vol. 62, pp. 21–28 (1962)Google Scholar
  92. [McC66]
    McCarthy, J.: A formal description of a subset of ALGOL. In: Formal Language Description Languages for Computer Programming, pp. 1–12. North-Holland (1966)Google Scholar
  93. [Men64]
    Mendelson, E.: Introduction to Mathematical Logic. van Norstrand (1964)Google Scholar
  94. [Mey88]
    Meyer, B.: Object-Oriented Software Construction. Prentice-Hall, Upper Saddle River (1988)Google Scholar
  95. [Mil89]
    Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)zbMATHGoogle Scholar
  96. [Mog89]
    Moggi, E.: An abstract view of programming languages. Ph.D. thesis, Laboratory for the Foundation of Computer Science, Edinburgh University (1989)Google Scholar
  97. [Mor94]
    Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice Hall, Upper Saddle River (1994)zbMATHGoogle Scholar
  98. [Mos11]
    Mosses, P.D.: VDM semantics of programming languages: combinators and monads. Form. Asp. Comput. 23(2), 221–238 (2011)MathSciNetCrossRefGoogle Scholar
  99. [MP67]
    McCarthy, J., Painter, J.: Correctness of a compiler for arithmetic expressions. Math. Asp. Comput. Sci. 19 (1967)Google Scholar
  100. [MS74]
    Milne, R., Strachey, C.: A theory of programming language semantics. Privately circulated (1974). Submitted for the Adams PrizeGoogle Scholar
  101. [MS76]
    Milne, R., Strachey, C.: A Theory of Programming Language Semantics (Parts A and B). Chapman and Hall, Boca Raton (1976)zbMATHGoogle Scholar
  102. [NK13]
    Nipkow, T., Klein, G.: Concrete Semantics. A Proof Assistant Approach. Springer, Cham (2013)Google Scholar
  103. [NN92]
    Nielson, H.R., Nielson, F.: Semantics with Applications: A Formal Introduction. Wiley, New York (1992)zbMATHGoogle Scholar
  104. [O’H07]
    O’Hearn, P.W.: Resources, concurrency and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007)MathSciNetCrossRefGoogle Scholar
  105. [Pag81]
    Pagan, F.G.: Formal Specification of Programming Languages. Prentice-Hall, Upper Saddle River (1981)zbMATHGoogle Scholar
  106. [Pai67]
    Painter, J.A.: Semantic correctness of a compiler for an ALGOL-like language. Technical report AI Memo 44, Computer Science Department, Stanford University, March 1967Google Scholar
  107. [Par10]
    Parkinson, M.: The next 700 separation logics. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 169–182. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15057-9_12CrossRefGoogle Scholar
  108. [Pat67]
    Paterson, M.S.: Equivalence problems in a model of computation. Ph.D. thesis, University of Cambridge (1967)Google Scholar
  109. [Pie02]
    Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)zbMATHGoogle Scholar
  110. [Plo76]
    Plotkin, G.D.: A powerdomain construction. SIAM J. Comput. 5, 452–487 (1976)MathSciNetCrossRefGoogle Scholar
  111. [Plo81]
    Plotkin, G.D.: A structural approach to operational semantics. Technical report DAIMI FN-19, Aarhus University (1981)Google Scholar
  112. [Pra65]
    Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Dover Publications, New York (1965)zbMATHGoogle Scholar
  113. [Rey78]
    Reynolds, J.C.: Syntactic control of interference. In: Proceedings of Fifth POPL, pp. 39–46. ACM (1978)Google Scholar
  114. [Rey89]
    Reynolds, J.C.: Syntactic control of interference part 2. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 704–722. Springer, Heidelberg (1989).  https://doi.org/10.1007/BFb0035793CrossRefGoogle Scholar
  115. [RR62]
    Randell, B., Russell, L.J.: Discussions on ALGOL translation at Mathematisch Centrum. English Electric Report W/AT, 841 (1962)Google Scholar
  116. [San99]
    Sangiorgi, D.: Typed pi-calculus at work: a correctness proof of Jones’s parallelisation transformation on concurrent objects. TAPOS 5(1), 25–33 (1999)MathSciNetGoogle Scholar
  117. [Sco80]
    Scott, D.: Lambda calculus: some models, some philosophy. Stud. Log. Found. Math. 101, 223–265 (1980)MathSciNetCrossRefGoogle Scholar
  118. [Smy76]
    Smyth, M.B.: Powerdomains. Technical report, Department of Computer Science, University of Warwick, May 1976Google Scholar
  119. [Spi88]
    Spivey, J.M.: Understanding Z—A Specification Language and its Formal Semantics. Cambridge Tracts in Computer Science 3. Cambridge University Press (1988)Google Scholar
  120. [Ste66]
    Steel, T.B.: Formal Language Description Languages for Computer Programming. North-Holland, London (1966)zbMATHGoogle Scholar
  121. [Sto77]
    Stoy, J.E.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge (1977)zbMATHGoogle Scholar
  122. [SW01]
    Sangiorgi, D., Walker, D.: The \(\pi \)-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  123. [Tur49]
    Turing, A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, pp. 67–69. University Mathematical Laboratory, Cambridge, June 1949Google Scholar
  124. [Tur09]
    Turner, R.: The meaning of programming languages. Am. Philos. Assoc. Newsl. Philos. Comput. 9(1), 2–6 (2009)Google Scholar
  125. [vdH17]
    van den Hove, G.: New insights from old programs: the structure of the first ALGOL 60 system. Ph.D. thesis, University of Amsterdam (2017)Google Scholar
  126. [vWMPK69]
    van Wijngaarden, A., Mailloux, B.J., Peck, J.E.L., Koster, C.H.A.: Report on the algorithmic language ALGOL 68. Mathematisch Centrum, Amsterdam, October 1969. Second printing, MR 101Google Scholar
  127. [WAB+68]
    Walk, K., et al.: Abstract syntax and interpretation of PL/I. Technical report 25.082, IBM Laboratory Vienna, ULD Version II, June 1968Google Scholar
  128. [Wal67]
    Walk, K.: Minutes of the 1st meeting of IFIP WG 2.2 on Formal Language Description Languages. Kept in the van Wijngaarden archive: Held in Porto Conte. Alghero, Sardinia (1967)Google Scholar
  129. [Wal69]
    Walk, K.: Minutes of the 3rd Meeting of IFIP WG 2.2 on Formal Language Description Languages, April 1969. Held in Vienna, AustriaGoogle Scholar
  130. [Wei75]
    Weissenböck. F.: A formal interface specification. Technical report TR 25.141, IBM Laboratory Vienna, February 1975Google Scholar
  131. [Win93]
    Winskel, G.: The Formal Semantics of Programming Languages. The MIT Press (1993). ISBN 0-262-23169-7Google Scholar
  132. [Woo93]
    Woodman, M.: A taste of the Modula-2 standard. ACM SIGPLAN Not. 28(9), 15–24 (1993)CrossRefGoogle Scholar
  133. [Yon90]
    Yonezawa, A. (ed.): ABCL: An Object-Oriented Concurrent System. MIT Press, Cambridge (1990). ISBN 0-262-24029-7Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.School of ComputingNewcastle UniversityNewcastle upon TyneUK

Personalised recommendations