Abstract
The programming language ALGOL 60 has been used to illustrate several different styles of formal semantic description. This paper identifies the main challenges in providing formal semantics for imperative programming languages and reviews the responses to these challenges in four relatively complete formal descriptions of ALGOL 60. The aim is to identify the key concepts rather than become distracted by the minutiae of notational conventions adopted by their authors. This paper also explores the historical reasons for the development of these descriptions in particular, and gives some general historical background of the groups involved (the IBM laboratories in Vienna and Hursley, and Oxford’s Programming Research Group).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Many authors use the phase “formal definition”; following Peter Mosses, we reserve “definition” for a document that is an established standard. Most formal semantic descriptions are separate from the standard (and written after it is set).
- 2.
Henceforth, unqualified references to ‘ALGOL’ are to be taken to refer to ALGOL 60.
- 3.
In places where it is useful to establish a link to later work the forward references are placed in footnotes.
- 4.
All but one of the ALGOL descriptions are only available as technical reports and there was never an easy path to publishing the descriptions of even larger languages. Where the authors have access to physical copies of historical documents that are difficult to locate, they have made scans available at: http://homepages.cs.ncl.ac.uk/cliff.jones/semantics-library/. In particular, all four descriptions of ALGOL are available.
- 5.
More recent ‘relaxed’ (or weak) memory architectures have, however, made this much harder.
- 6.
A panel, on which Jones sat, at the Mathematical Foundations of Programming Semantics held at CMU in 2004 was asked an interesting two-part question by Vaughan Pratt: (1) How much money have high-level programming languages saved the world? (2) Is there a Nobel Prize in Economics for answering (1)?
- 7.
It is interesting that the term ‘compiler’ is more commonly used than ‘translator’; the former appears to derive from the early attempts to improve re-use of programs by building libraries of routines that could be compiled with some additions to create an application. According to Grace Hopper, a key member of the team that created the very first such compilers, this was a precursor to actual languages where the task was more clearly one of translation (Beyer 2009, p. 223).
- 8.
An indication of the scale of the challenge is that up to 2010, a web site that attempted to track programming languages had recorded 8512 languages (and this probably excluded myriad ‘domain specific languages’).
- 9.
There is a distinction to be made between concrete and abstract syntax. Concrete syntax defines the valid texts of a language in terms of strings of symbols of the language. Abstract syntax uses a different notation to describe the syntax of a language purely in terms of its composition from subcomponents. Furthermore, the fact that either syntactic description is likely to be context free means that context dependencies have to be recorded separately. Some approaches handle such constraints statically in ‘context conditions’ whereas others detect inconsistent uses of declared variables dynamically (i.e. in the semantic rules).
- 10.
See the discussion raised by McCarthy in a paper presented in 1964 (McCarthy 1966, §8).
- 11.
See the discussion in Sect. 4.7.1 about non-deterministic languages that require a way of saying that there is more than one valid result to a computation.
- 12.
- 13.
For reasons of length, several topics that are covered in the Technical Report version (Jones and Astarte 2016) are omitted here.
- 14.
These sections also deviate from historical convention by making references to subsequent research that was affected by work being discussed.
- 15.
(Perlis 1981, p. 91) quips “ALGOL deserves our affection and appreciation. It was a noble begin but never intended to be a satisfactory end.”.
- 16.
A major impetus to research on Programming Methodology arose from the divisions surrounding ALGOL-68: IFIP WG 2.3 was formed around distinguished figures such as Dahl, Dijkstra and Hoare who signed the “minority report” in WG 2.1. This is not the place to repeat this story—see the ALGOL 68 session in the second History of Programming Languages conference (Bergin and Gibson 1996); another account is given in Chapter 7 of Pel´aez’ thesis (Pel´aez Valdez 1988).
- 17.
The author also notes that ‘Algol’ is the name of a fixed star in the Perseus constellation; it is an Arabic word whose meaning is ‘the demon’. This pun was not lost on the original language designers! (Pel´aez Valdez 1988, p. 26).
- 18.
Precisely how this is handled depends on implementation and definition, but the essential idea of these values being non-accessible remains.
- 19.
The ALGOL literature tends to refer to arguments as ‘actual parameters’ and to parameters as ‘formal parameters’.
- 20.
Christopher S. Strachey (1916–1975); leading British computer scientist who published little but each item was a polished gem (e.g. ‘The varieties of programming language’ (Strachey 1973), which became something of a manual to those interested in programming theory); see Martin Campbell-Kelly’s ‘Biographical Note’ (Campbell-Kelly 1985) for an excellent biographical summary.
- 21.
Some people argue that because labels are types, and values of other types (such as integer) can be assigned to variables, there should be variables to which one can assign label values.
- 22.
- 23.
Letter dated 1974-03-26 from Syracuse University (USA) held in the Bodleian archive of Strachey’s papers.
- 24.
Some authors use the term ‘static semantics’ for these context conditions (and ‘dynamic semantics’ for what below is called simply ‘semantics’). These terms are not employed in this paper.
- 25.
That said, Peter Naur attacked Henhapl and Jones in his paper ‘Formalization in program development’ (Naur 1981b), after publication of the duo’s ALGOL description (Henhapl and Jones 1978) (see Sect. 4.6), comparing the complicated mathematics of the formal model unfavourably to the structured English of the ‘Modified Report’ (de Morgan et al. 1976a).
- 26.
John McCarthy (1927–2011); AI pioneer and inventor of LISP. See http://news.stanford.edu/news/2011/october/john-mccarthy-obit-102511.html for one obituary.
- 27.
Heinz Zemanek (1920–2014); Austrian computing pioneer; see Fröschl et al. (2015) for an In Memoriam.
- 28.
The start of an influential series— for decades, IFIP Working Conferences provided one of the main drivers for researchers.
- 29.
In the Preface to the proceedings, the editor Tom Steel observes “Attendance was limited by invitation to recognised experts in one or more of the various disciplines of linguistics, logic, mathematics, philosophy, and programming whose frontiers converge around the subject of the meeting. The resulting group—51 individuals from 12 nations—was ideal in size, breadth of experience, and commitment to the enterprise.”
- 30.
In a sense, this can be seen as the germ of the ULD ‘control tree’ (see Sect. 4.3.5.4).
- 31.
Strictly, the program counter is Curried but no essential use is made of this higher order idea.
- 32.
Contributions are acknowledged from other members of the laboratory: Lucas, Alber, Bekič, and Fleck.
- 33.
Zemanek consistently encouraged his staff to obtain their doctorates. Erich Neuhold gratefully recalled the major influence that this had on his career (personal communication December 2016).
- 34.
- 35.
Bo Evans is franker: in his unpublished autobiographical notes, he writes “IBM undertook to specify and develop a single high-level language, PL/I, to serve both types of applications, something that could replace FORTRAN and COBOL”.
- 36.
There was a parallel activity in the IBM Böblingen Laboratory to develop a PL/I compiler for smaller IBM/360 machines; see Albert Endres’ history of early language development in Europe at IBM (Endres 2013).
- 37.
Personal communication, 2016.
- 38.
Maurer; Neuhold; Kurt Walk (personal communications in December 2016).
- 39.
As recorded in History of Programming Languages, this language was to have been called ‘New Programming Language’ or NPL until the (UK) National Physical Laboratory pointed out their prior use of the abbreviation (Radin 1981). Note also the title of an early paper discussing the language: ‘NPL: highlights of a new programming language’ (Radin and Rogoway 1965).
- 40.
The material here was reinforced by a discussion with David Beech when he visited Newcastle on 2016-08-12.
- 41.
This survey also puts an emphasis on the notion of VDL ‘objects’ that might surprise a current reader of the material.
- 42.
For a detailed description of this work on storage formalisation, see (Bekič and Walk 1971) since it does not relate to ALGOL.
- 43.
Versions II and III of ULD-III (as well as ULD-II) have been scanned and are available (see footnote 4); in addition there were a number of revisions made to ULD-III v-III, these are also on the web pages.
- 44.
This is evidenced by his choice of an ALGOL 60 compiler for Mailüfterl as a demonstration of its capability of handling high-level languages.
- 45.
Page numbers in the report are split by chapter.
- 46.
This can be compared with the more straightforward notation for such composite objects in the Vienna group’s later VDM style; see Sect. 4.6.
- 47.
The later ‘functional’ description discussed in Sect. 4.4.3.3 follows a similar system but does have some static checking.
- 48.
A technical penalty for using grand state descriptions is discussed in Sect. 4.4.
- 49.
In contrast to the signature for McCarthy’s which used Σ for the set of all possible stores, Ξ is used here to emphasise that VDL states contain much more than the store (see below).
- 50.
- 51.
Technically, Lucas’ approach to establishing equivalence was to combine the states of the two algorithms and link them by what we would call today a data type invariant; having then shown that the combined machine preserves this invariant, Lucas used the lovely phrase that one could then “erase the algorithm that one no longer required”.
- 52.
Clifford Bryn Jones (b. 1944); worked in the computer industry (including 15 years at IBM) straight out of school and later completed a belated D.Phil. under Hoare at Oxford (Wolfson College) in 1981.
- 53.
One of Jones’ first activities was to review Lauer’s ALGOL description prior to its printing, so he had a good degree of familiarity with the VDL.
- 54.
First available as a Vienna Lab technical report (TR25.110) in August 1970 immediately before Jones moved back to the UK. Two other relevant reports that explored some alternative implementations of the block concept are Henhapl and Jones (1970a, 1971). In 2017, Jones was surprised to note that Jones and Lucas (1971) still used Lucas’ twin machine approach because he had noted the benefits of a functional relation in Jones (1970) (Robin Milner used the more mathematical term ‘homomorphism’ in Milner 1971 and Hoare also used a functional connection in Hoare 1972). VDM later used the term ‘retrieve functions’ for the connection between representation and abstraction.
- 55.
Later, before Jones returned to Vienna in early 1973, they worked on an early ‘Formal Development Support System’: FDSS was an attempt to build support for program verification using proof obligations for relational post conditions that eventually crystallised in program development aspects of VDM.
- 56.
- 57.
This concept was to play a major part in the VDM style of denotational semantics (see Sect. 4.6), but in this ‘functional’ description it was presented in a rather verbose form.
- 58.
This eventually led to the ‘context conditions’ seen in the VDM Denotational description (see Sect. 4.6.3).
- 59.
This is precisely the reaction to the problems discussed above with respect to the proofs in Jones and Lucas (1971).
- 60.
This was later resolved by the VDM ‘combinators’ discussed in Sect. 4.6.4.
- 61.
Variously also referred to as ‘mathematical’ or ‘Scott-Strachey’ semantics.
- 62.
Dana S. Scott (b. 1932); American mathematician and logician who studied under Tarski and was awarded the Turing award in 1976 for his joint work with Michael O. Rabin on finite automata.
- 63.
Peter David Mosses (b. 1948); D.Phil. under Strachey; spent 1976–2004 at Aarhus University in Denmark.
- 64.
Peter Mosses, personal communication June 2016.
- 65.
This is another document that has been scanned and is available on-line.
- 66.
Roger Penrose (b. 1931); renowned mathematician and physicist; Fellow of Wolfson College at the time of its formation (as was Strachey).
- 67.
In this CV, Strachey notes “It is an interesting comment on the state of the subject that this work which at the time was probably the only work of its sort being carried out anywhere (certainly anywhere in England) was being financed privately by me.” (also quoted by Campbell-Kelly 1985).
- 68.
- 69.
A draft of this paper is contained in the archive of Strachey’s papers in the Bodleian Library and it is clear that it was completely written prior to the meeting in 1964.
- 70.
Both Scott and Jones were invited to give papers at the conference in 1983 that marked its renaming to Centrum Wiskunde & Informatica.
- 71.
One major issue is the ‘cardinality problem’: the number of functions \(\mathbb {N}\to \mathbb {N}\) must have a higher cardinality than that of \(\mathbb {N}\). Thus, there are more procedures over \(\mathbb {N}\) than ℵ 0. If one associates an untyped λ-defined function with procedures that can be passed as arguments to themselves a paradox is likely. Scott resolved the problem by posing suitable restrictions on functions so that domains could be constructed that can be viewed as partially ordered lattices.
- 72.
Talks given at the Strachey 100 centenary symposium in November 2016.
- 73.
John Charles Reynolds (1935–2013); a profound contributor whose nominations for the Turing Prize were never rewarded, he was Professor at Syracuse from 1970–86 and at CMU from 1986 until his untimely death.
- 74.
Most denotational semantics publications (e.g. Stoy’s textbook Stoy 1977) credit Wadsworth and also Lockwood Morris independently; the story is, however, slightly more complicated: see Reynolds (1993) for a fuller history. Reynolds’ work was updated somewhat in his December 2004 talk at the Computer Conservation Society in London. Video recordings exist of this event and the earlier one organised in the same way in June 2001.
- 75.
Milne remarked in his talk at the Strachey centenary conference that having spent two or three years working on the book, he then returned to the subject of formal semantics only very intermittently in the next 40 years (Milne 2016).
- 76.
Meaning that compositionality is preserved: the denotation of
is equal to the denotation of 
. - 77.
The name ‘Vienna Development Method’ was actually coined rather late in the project. There is also a certain ambiguity: to many people, VDM refers to a development method for all forms of computer system (this aspect is placed in a historical context in Jones’ Annals of the History of Computing paper on the history of program verification, see Jones 2003); in the current paper, VDM is taken to refer specifically to the technique for language description that evolved in and from work in the Vienna Lab between 1973 and 1976.
- 78.
An interesting cautionary tale about formal descriptions relates to that of the FS architecture itself. As indicated, the architecture was novel and quite complicated. Clearly, to design a compiler, it was necessary to have a clear description of the (evolving) architecture. A small team in the IBM Lab in Poughkeepsie (New York State) wrote a formal description that initially used rather abstract types and implicit definitions. This was not, of course, executable. Management suggested that since this had involved a lot of work (and thus expense) it would be better if it could execute FS instructions. The team laboured to achieve this and then to respond to a subsequent request that it should be optimised to run at a more acceptable speed. At the end of this process, the long and detailed description was of little use to the Vienna Lab as a basis for reasoning about the run-time part of their compiler for the FS machine and Hans Bekič had to write a short formal description to guide the compiler code generation work.
- 79.
According to an oral history with Dick Case (Grad 2006).
- 80.
There is a coda to this story. At that time, Springer Verlag appeared to take the attitude that once an LNCS volume had sold its initial print run that their task was complete. When they declined to reprint LNCS 61, Tony Hoare came to the rescue and offered to have a suitably updated collection of papers reprinted in his prestigious ‘red and white’ Prentice-Hall series: Bjørner and Jones (1982) contains among other contributions a revised description of ALGOL by the same authors (Henhapl and Jones 1982). The revision differs mainly in the order of presentation.
- 81.
The PL/I description appears to be the first published use of a completely formalised static error checking system.
- 82.
This is close to the style of the Prentice-Hall reprint but the original description used a more long-winded notation.
- 83.
Peter Mosses in a later paper (Mosses 2011) points out that the use of combinators in VDM is similar to the later development of Moggi’s ‘monads’ (Moggi 1989). The use of combinators also makes denotational descriptions in VDM look different from those written in Oxford where arguments (with very short names) are passed to Curried functions.
- 84.
Interestingly, also in Plotkin (2004b) he adds: “I recall Dana [Scott] …asked a good question: why call it operational semantics? What is operational about it? It would be interesting to know the origins of the term ‘operational semantics’; an early use is in a paper of Dana’s …written in the context of discussions with Christopher Strachey where they came up with the denotational/operational distinction. The Vienna group did discuss operations in their publications, meaning the operations of the abstract interpreting machine, but do not seem to have used the term itself.”
- 85.
Again from Plotkin (2004b): “A realisation struck me around then. I, and others, were writing papers on denotational semantics, proving adequacy relative to an operational semantics. But the rule-based operational semantics was both simple and given by elementary mathematical means. So why not consider dropping denotational semantics and, once again, take operational semantics seriously as a specification method for the semantics of programming languages?”
And again: “The second idea was that the rules should be syntax-directed; this is reflected in the title of the Aarhus notes: the operational semantics is structural, not, as some took it, structured. In denotational semantics one follows an ideal of compositionality, where the meaning of a compound phrase is given as a function of the meaning of its parts.”
- 86.
The decision not to record the types of the semantic functions makes checking VDL definitions more tedious that it needed to be.
- 87.
Personal communication, December 2016.
- 88.
Personal communication, June 2016.
- 89.
The description omits call by name, procedures and arrays as parameters, own variables and switches.
is equal to the denotation of 
.References
Alber, K., and P. Oliva. 1968. Translation of PL/I into abstract syntax. Technical Report 25.086, IBM Laboratory Vienna, ULD-IIIvII, June 1968.
Alber, K., P. Oliva, and G. Urschler. 1968. Concrete syntax of PL/I. Technical Report 25.084, IBM Laboratory Vienna, ULD-IIIvII, June 1968.
Alber, K., H. Goldmann, P.E. Lauer, P. Lucas, P. Oliva, H. Stigleitner, K. Walk, and G. Zeisel. 1969. Informal introduction to the abstract syntax and interpretation of PL/I. Technical Report 25.099, IBM Laboratory Vienna, ULD-IIIvIII, June 1969.
Allen, C.D., D. Beech, J.E. Nicholls, and R. Rowe. 1966. An abstract interpreter of PL/I. Technical Report TN 3004, IBM Laboratory Hursley, ULD-II, Nov 1966.
Allen, C.D., D.N. Chapman, and C.B. Jones. 1972. A formal definition of ALGOL 60. Technical Report 12.105, IBM Laboratory Hursley, Aug 1972. http://homepages.cs.ncl.ac.uk/cliff.jones/ftp-stuff/TR12.105.pdf
Andrews, D., and W. Henhapl. 1982. Pascal. In Bjørner and Jones (1982 ), chapter 6, pages 175–252. http://homepages.cs.ncl.ac.uk/cliff.jones/ftp-stuff/BjornerJones1982/Chapter-7.pdf.
Andrews, D., A. Garg, S. Lau, and J. Pitchers. 1988. The formal definition of Modula-2 and its associated interpreter. In VDM ’88 VDM—the way ahead, vol. 328, ed. R.E. Bloomfield, L.S. Marshall, and R.B. Jones. Lecture notes in computer science, 167–177. Berlin/Heidelberg: Springer.
ANSI. 1976. Programming language PL/I. Technical Report X3.53-1976, American National Standard.
Arbab, B., and D.M. Berry. 1987. Operational and denotational semantics of Prolog. The Journal of Logic Programming 4(4): 309–329.
Backus, J.W. 1959. The syntax and semantics of the proposed international algebraic language of the Zurich ACM-GAMM conference. In Proceedings of the international conference on information processing, 125–132. Paris: UNESCO.
Backus, J.W., F.L. Bauer, J. Green, C. Katz, J. McCarthy, P. Naur, A.J. Perlis, H. Rutishauser, K. Samelson, B. Vauquois. 1960. Report on the algorithmic language ALGOL 60. Numerische Mathematik 2(1): 106–136.
Backus, J.W., F.L. Bauer, J. Green, C. Katz, J. McCarthy, P. Naur, A.J. Perlis, H. Rutishauser, K. Samelson, B. Vauquois, J.H. Wegstein, A. van Wijngaarden, and M. Woodger. 1963. Revised report on the algorithm language ALGOL 60. Communications of the ACM 6(1): 1–17. http://homepages.cs.ncl.ac.uk/cliff.jones/publications/OCRd/BBG63.pdf
de Bakker, J.W., and D. Scott. 1969. A theory of programs. Manuscript notes for IBM Seminar, Vienna, Aug 1969.
Bandat, K. 1965. Tentative steps towards a formal description of PL/I. Technical Report 25.056, IBM Laboratory Vienna, July 1965.
Bandat, K., E.F. Codd, R.A. Larner, P. Lucas, J.E. Nicholls, and K. Walk. 1965. Unambiguous definition of PL/I. IBM internal memo, Oct 1965. Technical University of Vienna NL. 14. 072/2 Zemanek. PL/I History Documents.
Barron, D.W., J.N. Buxton, D.F. Hartley, and C. Strachey. 1963. The main features of CPL. Computer Journal 6: 134–143.
Beech, D., J.E. Nicholls, and R. Rowe. 1966. A PL/I translator. Technical Report TN 3003, IBM Laboratory Hursley, ULD-II, Oct 1966a.
Beech, D., R. Rowe, R.A. Larner, and J.E. Nicholls. 1966b. Concrete syntax of PL/I. Technical Report TN 3001, IBM Laboratory Hursley, ULD-II, Nov 1966.
Beech, D., R. Rowe, R.A. Larner, and J.E. Nicholls. 1967. Abstract syntax of PL/I. Technical Report TN 3002, IBM Laboratory Hursley, ULD-II, May 1967.
Bekič, H. 1964. Defining a language in its own terms. Technical Report 25.3.016, IBM Laboratory Vienna, Dec 1964.
Bekič, H. 1971. Towards a mathematical theory of processes. Technical Report TR 25.125, IBM Laboratory Vienna, 1971.
Bekič, H., and K. Walk. 1971. Formalization of storage properties. In Symposium on semantics of algorithmic languages, vol. 188, ed. E. Engeler. Lecture notes in mathematics, 28–61. Berlin: Springer.
Bekič, H., D. Bjørner, W. Henhapl, C.B. Jones, and P. Lucas. 1974. A formal definition of a PL/I subset. Technical Report 25.139, IBM Laboratory Vienna, Dec 1974. http://homepages.cs.ncl.ac.uk/cliff.jones/ftp-stuff/TR25139/
Bekič, H., H. Izbicki, C.B. Jones, and F. Weissenböck. 1975. Some experiments with using a formal language definition in compiler development. Technical Report LN 25.3.107, IBM Laboratory Vienna, Dec 1975.
Bergin, T.J., and R.G. Gibson, ed. 1996. History of programming languages—II. New York: ACM Press.
Beyer, K.W. 2009. Grace Hopper and the invention of the information age. Cambridge, Massachusetts: The MIT Press.
Bjørner, D., and C.B. Jones, ed. 1978. The Vienna development method: The meta-language, vol. 61. LNCS. Berlin/Heidelberg: Springer.
Bjørner, D., and C.B. Jones, ed. 1982. Formal specification and software development. Englewood Cliffs: Prentice Hall International. http://homepages.cs.ncl.ac.uk/cliff.jones/ftp-stuff/BjornerJones1982
Bjørner, D., and O.N. Oest. 1980. Towards a formal description of Ada, vol. 98. LNCS. Berlin/Heidelberg: Springer.
Burstall, R.M. 1970. Formal description of program structure and semantics in first-order logic. Machine Intelligence 5: 79–98.
Campbell-Kelly, M. 1985. Christopher Strachey, 1916–1975: A biographical note. Annals of the History of Computing 7: 19–42.
Daylight, E.G. 2012. The dawn of software engineering: From Turing to Dijkstra. Belgium: Lonely Scholar. ISBN: 9491386026, 9789491386022.
Dijkstra, E.W. 1968. Letters to the editor: Go to statement considered harmful. Communications of the ACM 11(3): 147–148.
Duncan, F.G. 1963. ECMA subset of ALGOL 60. Communications of the ACM 6(10): 595–599.
Duncan, F.G. 1966. Our ultimate metalanguage: An afterdinner talk. In Formal language description languages for computer programming, ed. Thomas B Steel, 295–295. Amsterdam: North-Holland.
de Vere Roberts, M. 1965. Radiogram to Kurt Bandat. IBM internal memo, Sept 1965. Technical University of Vienna NL. 14. 072/2 Zemanek. PL/I History Documents.
ECMA. 1965. Standard ECMA-2 for a subset of ALGOL. Technical report, European Computer Manufacturers’ Association, 1965.
Endres, A. 2013. Early language and compiler developments at IBM Europe: A personal retrospection. Annals of the History of Computing, IEEE 35(4): 18–30.
Fleck, M. 1969. Formal definition of the PL/I compile time facilities. Technical Report 25.095, IBM Laboratory Vienna, ULD-IIIvIII, June 1969.
Fleck, M., and E. Neuhold. 1968. Formal definition of the PL/I compile time facilities. Technical Report 25.080, IBM Laboratory Vienna, ULD-IIIvII, June 1968.
Floyd, R.W. 1962. On the nonexistence of a phrase structure grammar for ALGOL 60. Communications of the ACM 5(9): 483–484.
Floyd, R.W. 1967. Assigning meanings to programs. In Proceedings of the symposium in applied mathematics, vol.19: Mathematical aspects of computer science, 19–32. Providence: American Mathematical Society.
Fröschl, K.A., G. Chroust, and J. Stockinger, eds. 2015. In memoriam Heinz Zemanek, volume Band-311. OCG, 2015.
Grad, B. 2006. Oral history of Richard Case. Online, 2006. http://archive.computerhistory.org/resources/text/Oral_History/Case_Richard/Case_Richard_1.oral_history.2006.102658006.pdf
Hansal, A. 1976. A formal definition of a relational data base system. Technical Report UKSC 0080, IBM UK Scientific Centre, Peterlee, Co. Durham, June 1976.
Henhapl, W., and C.B. Jones. 1970a. The block concept and some possible implementations, with proofs of equivalence. Technical Report 25.104, IBM Laboratory Vienna, Apr 1970.
Henhapl, W., and C.B. Jones. 1970b. On the interpretation of GOTO statements in the ULD. Technical Report 25.3.065, IBM Laboratory Vienna, Mar 1970.
Henhapl, W., and C.B. Jones. 1971. A run-time mechanism for referencing variables. Information Processing Letters 1(1): 14–16.
Henhapl, W., and C.B. Jones. 1978. A formal definition of ALGOL 60 as described in the 1975 modified report. In Bjørner and Jones, 1978, 305–336. http://homepages.cs.ncl.ac.uk/cliff.jones/publications/OCRd/HJ82.pdf
Henhapl, W., and C.B. Jones. 1982. ALGOL 60. In Bjørner and Jones, 1982, chapter 6, 141–174. http://homepages.cs.ncl.ac.uk/cliff.jones/ftp-stuff/BjornerJones1982
Hoare, C.A.R. 1969. An axiomatic basis for computer programming. Communications of the ACM 12(10): 576–580.
Hoare, C.A.R. 1972. Proof of correctness of data representations. Acta Informatica 1: 271–281.
Hoare, C.A.R. 1973. Hints on programming language design. Technical report, Stanford University, Stanford, 1973.
Hoare, C.A.R., and N. Wirth. 1973. An axiomatic definition of the programming language Pascal. Acta Informatica 2(4): 335–355.
IFIP. 1964. Working Conference Vienna 1964. Formal Language Description Languages. Program. Christopher Strachey Collection, Bodleian Library, Oxford. Box 287, E.39, Feb 1964.
Izbicki, H. 1975. On a consistency proof of a chapter of a formal definition of a PL/I subset. Technical Report 25.142, IBM Laboratory Vienna, Feb 1975.
Jones, C.B. 1969. A comparison of two approaches to language definition as bases for the construction of proofs. Technical Report 25.3.050, IBM Laboratory Vienna, Feb 1969.
Jones, C.B. 1970. A technique for showing that two functions preserve a relation between their domains. Technical Report LR 25.3.067, IBM Laboratory Vienna, Apr 1970.
Jones, C.B. 1976. Formal definition in compiler development. Technical Report 25.145, IBM Laboratory Vienna, Feb 1976.
Jones, C.B. 1978. Denotational semantics of goto: An exit formulation and its relation to continuations. In Bjørner and Jones, 1978, 278–304.
Jones, C.B. 1982. More on exception mechanisms. In Bjørner and Jones, 1982, chapter 5, 125–140. http://homepages.cs.ncl.ac.uk/cliff.jones/ftp-stuff/BjornerJones1982
Jones, C.B. 1999. Scientific decisions which characterize VDM. In FM’99—formal methods, vol. 1708 LNCS, 28–47. Berlin/Heidelberg: Springer.
Jones, C.B. 2003. The early search for tractable ways of reasoning about programs. IEEE, Annals of the History of Computing 25(2): 26–49.
Jones, C.B., and T.K. Astarte. 2016. An Exegesis of Four Formal Descriptions of ALGOL 60. Technical Report 1498, Newcastle University School of Computer Science, Sept 2016.
Jones, C.B., and P. Lucas. 1971. Proving correctness of implementation techniques. In A Symposium on algorithmic languages, ed. E. Engeler, vol. 188. Lecture notes in mathematics, 178–211. Berlin/Heidelberg: Springer.
Knuth, D.E. 1964. Backus normal form vs. backus naur form. Communications of the ACM 7(12): 735–736.
Knuth, D.E., and R.W. Floyd. 1971. Notes on avoiding “go to” statements. Information Processing Letters 1(1): 23–31.
Knuth, D.E., and L.T. Pardo. 1976. The early development of programming languages. Technical Report STAN-CS-76-562, Stanford University.
Landin, P.J. 1964. The mechanical evaluation of expressions. The Computer Journal 6(4): 308–320.
Landin, P.J. 1965a. A correspondence between ALGOL 60 and Church’s lambda-notation: Part I. Communications of the ACM 8(2): 89–101.
Landin, P.J. 1965b. A correspondence between ALGOL 60 and Church’s lambda-notation: Part II. Communications of the ACM 8(3): 158–167.
Landin, P.J. 1966. A formal description of ALGOL 60. In Formal language description languages for computer programming, ed. Thomas B Steel, 266–290. Amsterdam: North Holland.
Larner, R.A., and J.E. Nicholls. 1965. Plan for development of formal definition of PL/I. IBM internal memo, Sept 1965. Technical University of Vienna NL. 14. 072/2 Zemanek. PL/I History Documents.
Lauer, P.E. 1967. The formal explicates of the notion of algorithm: An introduction to the theory of computability with special emphasis on the various formalisms underlying the alternate explicates. Technical Report 25.072, IBM Laboratory Vienna.
Lauer, P.E. 1968a. Formal definition of ALGOL 60. Technical Report 25.088, IBM Laboratory Vienna, Dec 1968. http://homepages.cs.ncl.ac.uk/cliff.jones/publications/OCRd/Lau68.pdf
Lauer, P.E. 1968b. An introduction to H. Thiele’s notions of algorithm, algorithmic process, and graph schemata calculus. Technical Report TR 25.079, IBM Laboratory Vienna, Jan 1968.
Lauer, P.E. 1971. Consistent Formal Theories of the Semantics of Programming Languages. Ph.D. thesis, Queen’s University of Belfast, 1971. Printed as TR 25.121, IBM Laboratory Vienna.
Lee, J.A.N. 1972. The formal definition of the BASIC language. The Computer Journal 15(1): 37–41.
Lee, J.A.N., and W. Delmore. 1969. The Vienna definition language, a generalization of instruction definitions. In SIGPLAN Symposium on Programming Language Definitions, San Francisco.
Lucas, P. 1968. Two constructive realisations of the block concept and their equivalence. Technical Report 25.085, IBM Laboratory Vienna, June 1968.
Lucas, P. 1981. Formal semantics of programming languages: VDL. IBM Journal of Research and Development 25(5): 549–561.
Lucas, P., and K. Walk. 1969. On the formal description of PL/I. Annual Review in Automatic Programming 6: 105–182.
Lucas, P., K. Alber, K. Bandat, H. Bekič, P. Oliva, K. Walk, and G. Zeisel. 1968a. Informal introduction to the abstract syntax and interpretation of PL/I. Technical Report 25.083, IBM Laboratory Vienna, ULD-IIIvII, June 1968.
Lucas, P., P.E. Lauer, and H. Stigleitner. 1968b. Method and notation for the formal definition of programming languages. Technical Report 25.087, IBM Laboratory Vienna, ULD-IIIvII, June 1968. http://homepages.cs.ncl.ac.uk/cliff.jones/publications/VDL-TRs/TR25.087.pdf
McCarthy, J. 1962. Towards a mathematical science of computation. In IFIP Congress, 21–28.
McCarthy, J. 1966. A formal description of a subset of ALGOL. In Formal language description languages for computer programming, ed. Thomas B Steel, 1–12. Amsterdam: North-Holland.
McCarthy, J. 1981. History of LISP. In History of programming languages, ed. R.L. Wexelblat, chapter 4, 173–183. New York: Academic.
McCarthy, J., and J. Painter. 1966. Correctness of a compiler for arithmetic expressions. Technical Report CS38, Computer Science Department, Stanford University, Apr 1966. See also pages 33–41 Proceedings of the symposium in applied mathematics, vol. 19: Mathematical aspects of computer science. Providence: American Mathematical Society.
Milne, R.E. 2016. Semantic relationships: Reducing the separation between practice and theory. Unpublished, Nov 2016. Talk given at Strachey 100 centenary conference.
Milne, R.E., and C. Strachey. 1974. A theory of programming language semantics. Privately circulated, 1973. An essay submitted for the Adams Prize 1973–1974.
Milne, R.E., and C. Strachey. 1976a. A theory of programming language semantics. London: Chapman and Hall. Part A: Indices and Appendices, Fundamental Concepts and Mathematical Foundations.
Milne, R.E., and C. Strachey. 1976b. A theory of programming language semantics. London: Chapman and Hall. Part B: Standard Semantics, Store Semantics and Stack Semantics.
Milner, R. 1971. An algebraic definition of simulation between programs. Technical Report CS-205, Computer Science Dept, Stanford University, Feb 1971.
Moggi, E. 1989. An abstract view of programming languages. Technical Report ECS-LFCS-90-113, Edinburgh University Laboratory for the Foundation of Computer Science.
de Morgan, R.M., I.D. Hill, and B.A. Wichmann. 1976a. Modified report on the algorithmic language ALGOL 60. The Computer Journal 19(4): 364–379.
de Morgan, R.M., I.D. Hill, and B.A. Wichmann. 1976b. A supplement to the ALGOL 60 revised report. The Computer Journal 19(3): 276–288.
Mosses, P.D. 1974. The mathematical semantics of ALGOL 60. Technical Monograph PRG-12, Oxford University Computing Laboratory, Programming Research Group, Ja 1974. http://homepages.cs.ncl.ac.uk/cliff.jones/publications/OCRd/Mosses74.pdf
Mosses, P.D. 1975a. The semantics of semantic equations. In Mathematical foundations of computer science: 3rd symposium at Jadwisin near Warsaw, 17–22 June 1974, ed. A. Blikle, 409–422. Berlin/Heidelberg. Springer.
Mosses, P.D. 1975b. Mathematical semantics and compiler generation. Ph.D. thesis, University of Oxford, Apr 1975.
Mosses, P.D. 2004. Modular structural operational semantics. The Journal of Logic and Algebraic Programming 60: 195–228.
Mosses, P.D. 2005. Action semantics, vol. 26. Cambridge/New York: Cambridge University Press.
Mosses, P.D. 2011. VDM semantics of programming languages: Combinators and monads. Formal Aspects of Computing 23(2): 221–238.
Mosses, P.D., and F. Vesely. 2014. Funkons: Component-based semantics in K. In Rewriting logic and its applications, ed. S. Escobar, 213–229. Cham: Springer.
Naur, P. 1981a. The European side of the last phase of the development of ALGOL 60. In History of programming languages, ed. R.L. Wexelblat, chapter 3, 92–137. New York: Academic.
Naur, P. 1981b. Formalization in program development. BIT Numerical Mathematics 22(4): 437–453.
Naur, P., and B. Randell. 1969. Software Engineering: Report of a Conference Sponsored by the NATO Science Committee, Garmisch, Germany, 7–11 Oct 1968, Brussels, Scientific Affairs Division, NATO.
Ollongren, A. 1971. A theory for the objects of the Vienna definition language. Technical Report 25.123, IBM Laboratory Vienna, Sept 1971.
Pel´aez Valdez, M.E. 1988. A gift from Pandora’s box: The software crisis. Ph.D. thesis, University of Edinburgh, 1988.
Penrose, R. 2000. Reminiscences of Christopher Strachey. Higher-Order and Symbolic Computation 13(1): 83–84.
Perlis, A.J. 1981. The American side of the development of ALGOL. In History of programming languages, ed. R.L. Wexelblat, chapter 3, 75–91. New York: Academic.
PL/I Definition Group of the Vienna Laboratory. 1966. Formal definition of PL/I (Universal Language Document No. 3). Technical Report 25.071, IBM Laboratory Vienna, ULD-IIIvI, Dec 1966.
Plotkin, G.D. 1976. A powerdomain construction. SIAM Journal on Computing 5: 452–487.
Plotkin, G.D. 1981. A structural approach to operational semantics. Technical report, Aarhus University.
Plotkin, G.D. 2004a. A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60–61: 17–139.
Plotkin, G.D. 2004b. The origins of structural operational semantics. Journal of Logic and Algebraic Programming 60–61: 3–15.
Priestley, M. 2011. A science of operations: Machines, logic and the invention of programming. London: Springer Science & Business Media.
Radin, G. 1981. The early history and characteristics of PL/I. In History of programming languages, ed. R.L. Wexelblat, 551–589. New York: Academic.
Radin, G., and H.P. Rogoway. 1965. NPL: Highlights of a new programming language. Communications of the ACM 8(1): 9–17.
Radin, G., and P. Schneider 1976. An architecture for an extended machine with protected addressing. Technical Report 00.2757, IBM Poughkeepsie Lab, May 1976.
Randell, B. 2013. The origins of digital computers: Selected papers. Berlin/Heidelberg: Springer.
Reynolds, J.C. 1993. The discoveries of continuations. Lisp and Symbolic Computation 6(3–4): 233–247.
Schwarzenberger, F., and H. Zemanek. 1966. Editing algorithms for texts over formal grammars. Technical Report 25.066, IBM Laboratory Vienna, July 1966.
Scott, D. 1969. A type-theoretical alternative to CUCH, ISWIM, OWHY. Typed script—Oxford, Oct 1969.
Scott, D. 1970. The lattice of flow diagrams. Technical Report PRG-3, Oxford University Computing Laboratory, Programming Research Group, Nov 1970.
Scott, D. 1971a. Continuous lattices. Technical Report PRG-7, Oxford University Computing Laboratory, Programming Research Group, Aug 1971.
Scott, D. 1971b. The lattice of flow diagrams. In Symposium on Semantics of Algorithmic Languages, 311–366. Berlin: Springer.
Scott, D. 1973. Models for various type-free calculi. In Studies in logic and foundations of mathematics vol. 74 (Proceedings of the 4th international congress for logic, methodology and philosophy of science, Bucharest, 1971), ed. P. Suppes, L. Henkin, A. Joja, and G. Moisil, 158–187. Amsterdam: North Holland Publishing Company.
Scott, D. 2000. Some reflections on Strachey and his work. Higher-Order and Symbolic Computation 13(1): 103–114.
Scott, D. 2016. Greetings to the participants at “Strachey 100”. A talk read out at the Strachey 100 centenary conference, Nov 2016.
Scott, D., and C. Strachey. 1971. Toward a mathematical semantics for computer languages. Technical Monograph PRG-6, Oxford University Computing Laboratory, Programming Research Group.
Scott, D., and T. Traxler. 2015. Logic Lounge with Dana Scott. Online, June 2015. https://www.youtube.com/watch?v=nhc94A829qI Video interview.
Shustek, L. 2015. An interview with Fred Brooks. Communications of the ACM 58(11): 36–40.
Steel, T.B. 1966. Formal language description languages for computer programming. New York: North-Holland Publishing Company.
Stoy, J.E. 1977. Denotational semantics: The Scott-Strachey approach to programming language theory. Cambridge: MIT Press.
Stoy, J.E. 1980. Foundations of denotational semantics. In Proceedings of the abstract software specifications: 1979 copenhagen winter school Jan 22–Feb 2 1979, ed. D. Bjørner, 43–99. Berlin/Heidelberg: Springer.
Strachey, C. 1966a. System analysis and programming. Scientific American 215: 112–124.
Strachey, C. 1966b. Towards a formal semantics. In Formal language description languages for computer programming, ed. Thomas B Steel. Amsterdam: North Holland.
Strachey, C. 1970. Jumping into and out of expressions, Aug 1970. Unpublished note. Strachey Papers, Bodleian Library, Oxford. Folder C229.
Strachey, C. 1971a. Curriculum vitae, Dec 1971. Written by Strachey to send to the times newspaper in case of the need for obitual information. Strachey Papers, Bodleian Library, Oxford. Folder A3.
Strachey, C. 1971b. Letter to Lord Halsbury, Oct 1971. Strachey Papers, Bodleian Library, Oxford. Folder A3.
Strachey, C. 1973. The varieties of programming language. Technical Monograph PRG-10, Oxford University Computing Lab, Mar 1973.
Strachey, C., and C.P. Wadsworth. 1974. Continuations—a mathematical semantics for handling jumps. Monograph PRG-11, Oxford University Computing Laboratory, Programming Research Group, Jan 1974.
Strachey, C., and M.V. Wilkes. 1961. Some proposals for improving the efficiency of ALGOL 60. Communications of the ACM 4(11): 488–491.
Tennent, R.D. 1976. The denotational semantics of programming languages. Communications of the ACM 19: 437–453.
Urschler, G. 1969a. Concrete syntax of PL/I. Technical Report 25.096, IBM Laboratory Vienna, ULD-IIIvIII, June 1969.
Urschler, G. 1969b. Translation of PL/I into abstract syntax. Technical Report 25.097, IBM Laboratory Vienna, ULD-IIIvIII, June 1969.
Utman, R.E. 1963. Minutes of the 3rd meeting of IFIP TC2. Online, Sept 1963. http://ershov-arc.iis.nsk.su/archive/eaindex.asp?did=41825. Chaired by H. Zemanek. Archived by Andrei Ershov.
Utman, R.E. 1964. Minutes of the 4th meeting of IFIP TC2. Online, May 1964. http://ershov-arc.iis.nsk.su/archive/eaindex.asp?did=41826. Chaired by H. Zemanek. Archived by Andrei Ershov.
van den Hove, G. 2014. On the origin of recursive procedures. The Computer Journal 58(11): 2892–2899.
Wadsworth, C.P. 1971. Semantics and pragmatics of the Lambda-Calculus. Ph.D. thesis, Programming Research Group, University of Oxford, Sept 1971.
Walk, K., K. Alber, K. Bandat, H. Bekič, G. Chroust, V. Kudielka, P. Oliva, and G. Zeisel. 1968. Abstract syntax and interpretation of PL/I. Technical Report 25.082, IBM Laboratory Vienna, ULD-IIIvII, June 1968.
Walk, K., K. Alber, M. Fleck, H. Goldmann, P.E.Lauer, E. Moser, P. Oliva, H. Stigleitner, and G. Zeisel. 1969. Abstract syntax and interpretation of PL/I. Technical Report 25.098, IBM Laboratory Vienna, ULD-IIIvIII, Apr 1969.
Wegner, P. 1972. The Vienna definition language. ACM Computing Surveys (CSUR) 4(1): 5–63.
Weissenböck, F. 1975. A formal interface specification. Technical Report 25.141, IBM Laboratory Vienna, Feb 1975.
Welsh, A. 1982. The specification, design and implementation of NDB. Master’s thesis, Department of Computer Science, University of Manchester, Oct 1982. Also published as technical report UMCS-82-10-1.
Welsh, A. 1984. A database programming language: definition, implementation and correctness proofs. PhD thesis, Department of Computer Science, University of Manchester, Oct 1984. Also published as technical report UMCS-84-10-1.
Wexelblat, R.L., ed. 1981. History of programming languages. New York: Academic.
Wichmann, B. 2004. The ALGOL bulletin, Feb 2004. http://archive.computerhistory.org/resources/text/algol/algol_bulletin/
Wilkinson, J.H. 1972. Letter to Christopher Strachey, Dec 1972. Strachey Papers, Bodleian Library, Oxford. Folder A3.
Wolczko, M.I. 1988. Semantics of object-oriented languages. Ph.D. thesis, Department of Computer Science, University of Manchester, Mar 1988. Also published as Technical Report UMCS-88-6-1.
Zemanek, H. 1968. Abstrakte objekte. Elektron. Rechenanl. 5: 208–217.
Zhang, Y., and B. Xu. 2004. A survey of semantic description frameworks for programming languages. ACM Sigplan Notices 39(3): 14–30.
Zimmermann, K. 1969. Outline of a formal definition of FORTRAN. Technical Report 25.3.053, IBM Laboratory Vienna, 1969.
Acknowledgements
The authors have benefited from detailed discussions with Peter Mosses, David Beech, Erich Neuhold, Kurt Walk, Gerhard Chroust, John Tucker and Joe Stoy; they are also grateful to Martin Campbell-Kelly for detailed comments on an early draft of the precursor technical report (Jones and Astarte 2016). An anonymous referee provided useful comments and Mark Priestly wrote a detailed and constructive review that has prompted significant changes to our initial submission.
Astarte would particularly like to thank the audience of the History and Philosophy of Programming 3 symposium in Paris in June 2016 for their useful questions and feedback after presentation of this work.
Jones began the detailed analysis of the ALGOL descriptions whilst collaborating with Peter Mosses on his PLanCompS project.
Thanks are also due to the Bodleian Library in Oxford for their archiving and curating of the Strachey papers, and to Juliane Mikoletzky at the Technical University of Vienna for information concerning the Zemanek Nachlass.
Financial support from EPSRC, who are both providing the PhD funding for Astarte and whose ‘Strata’ Platform Grant is funding travel expenses for both authors, is gratefully acknowledged.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Astarte, T.K., Jones, C.B. (2018). Formal Semantics of ALGOL 60: Four Descriptions in their Historical Context. In: De Mol, L., Primiero, G. (eds) Reflections on Programming Systems. Philosophical Studies Series, vol 133. Springer, Cham. https://doi.org/10.1007/978-3-319-97226-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-97226-8_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-97225-1
Online ISBN: 978-3-319-97226-8
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)