This volume contains historical and foundational material, and works on language design. All of the material should be accessible to beginning graduate students in programming languages and theoretical Computer Science.

The author had hoped to complete a formal description of the set of legal programs and of their meanings in time to present it here. Only the description of legal programs has been completed however. Therefore the formal treatment of the semantics of legal programs will be included in a subsequent paper.Backus goes on to introduce the meta-notation we now know as Backus-Naur formalism and uses it to specify the syntax of the language; however, the "subsequent paper" on the semantics never materialized, and the semantics is again described informally in the Revised Report on Algol 60[NB#63 ].

Many computer scientists today are unfamiliar with this important document, and so most of it has been included as Chapter 1 of this volume; subsequent corrections and discussion of various "ambiguities" may be found in [Knu67 , DHW76 ].

The importance of having precise descriptions of syntax and semantics is today generally appreciated; however, more than 35 years after Backus's talk, researchers are still trying to produce satisfactory descriptions of Algol-like languages. This situation is not unprecedented: mathematicians needed hundreds of years to sort out the semantic issues underlying the differential and integral calculi, and some thirty years passed between Alonzo Church's formulation of the (untyped) lambda calculus [Chu41 ] and the first mathematical models by Dana Scott [Sco72b].

Scott's work on the lambda calculus was partly motivated by a collaboration with Christopher Strachey [SS71] in which they outlined a "mathematical" approach to the semantics of procedural programming languages, using the powerful domain-theoretic tools Scott had developed. This approach, now termed denotational semantics, has become well known; a short introductory paper by Strachey has been included in this volume as Chapter 2.

In [SS71], Scott and Strachey had suggested that if "you put your domains on the table first" then this would help to reveal language-design issues and possibilities. This point of view is illustrated well by Strachey's chapter. The design of Algol 60 is compared to that of a language Pal with quite different domain structure. The comparison takes place exclusively on the level of domains appropriate to each language, independently of surface syntactic similarities or dissimilarities.

One of the most significant contributions to semantic analysis of programming languages by Strachey and his collaborators, such as Scott [Sco72a], Rod Burstall [Bur70], and Peter Landin [Lan65], is the distinction between the environment and the store (or state). The domain analysis of Algol 60 in Section 3.1 of Chapter 2 reveals the disjointness of the "storable" and "denotable" values in this language; this was later described by John Reynolds (see Chapter 3) as the distinction between "data types" and "phrase types."

In Strachey's paper, labels and jumps are not treated in any detail, but the important concept of continuations, which became the "standard" approach to these features, had already been discovered; see [SW74 , Rey93].

An unsatisfactory aspect of traditional denotational semantics for typed languages is that full advantage was not taken of syntactic typing information; for example, in the discussion of Algol 60 in Chapter 2, there is a single domain of all possible procedures, with "run-time" selection of the appropriate sub-domain.

Also, notice that the treatment of assignment is based on the low-level idea of "locations" or L-values,using global states with fixed structure. The approach to dynamic allocation adopted by Scott and Strachey is described in [Sco72a]; it is based on recording in every state which locations are currently "active" (i.e., in use). This has become known as the "marked-stores" approach.

A planned work by Strachey, "An abstract model of storage," referenced in both of these papers as being "in preparation", never appeared. (Strachey died in 1975.) More information on traditional denotational semantics may be found in [MS76 , Sto77].

a language so far ahead of its time that it was not only an improvement on its predecessors but also on nearly all its successors.Furthermore, Reynolds points out that most formal models of programming languages then in use were failing to do justice to typed languages and to important concepts such as representation-independent storage variables and stack-oriented storage management. As a result, languages designed with such models in mind would inevitably be influenced by concepts that are not truly Algol-like.

In more detail, Reynolds characterized "Algol-like" languages as follows.

- The procedure mechanism is based on the fully typed, call-by-name lambda calculus, and equational principles such as the fi and j laws are valid even in the presence of imperative features such as assignment commands and jumps.
- The language has assignments, but procedures, variables, and other denotable meanings are not assignable.
- Apart from overflow, roundoff error, and error stops, expressions are purely "mathematical," without non-local jumps, side effects, or ambiguous coercions.
- Allocation and de-allocation are based on a stack discipline, but the treatment of storage variables is otherwise representation independent.
- Generic features such as conditionals, recursion, and procedures are uniformly applicable to all types of phrases.

Syntactic and semantic descriptions tailored to this view of Algol-like languages differ significantly from that given by Strachey in Chapter 2. Syntactic descriptions must deal with an infinity of phrase types, and must take into account subtypes (coercions) which are not necessarily interpreted as subsets and which can introduce ambiguity. Typing contexts must be used to treat non-context-free constraints; a judgement of the form P \in <\theta,\pi> as used by Reynolds would today be written \pi \vdash P: \theta. Instead of using domains of all possible (infinitary) environments and all possible procedures, there is a domain of finitary environments for each assignment of types to finite sets of identifiers, and a domain of procedures for each type of argument and result.

A representation-independent view of storage variables is obtained by treating them as (acceptor, expression)pairs, where an acceptor can be viewed as a function mapping a storable value to a command meaning. This allows for parameterizing semantic domains and semantic interpretation functions by arbitrary sets of states. It is then possible to deal with local-variable declarations by "expanding" the set of states in use. This puts the stack-oriented nature of the language "on the table" at an early stage in the semantic defini tion. The general semantic framework can be presented quite elegantly using the category-theoretical notions of functors and natural transformations; see Part IV.

Chapters 4 to 7 formalize or develop in various ways some of the key ideas in "The Essence of Algol." Reynolds emphasized that the full beta and eta laws of the typed lambda calculus are valid in an Algol-like language, even for imperative phrases such as commands and variables. "Algol and Functional Programming" by Peter O'Hearn shows that an Algol-like language actually preserves all equivalences of the purely functional fragment, provided "snap-back" operations do not exist. An example of a "snap-back" operation would be a block expression in which a command is executed as part of the evaluation of an expression, but, because of possible side-effects to non-local variables, the initial state for that execution is then restored. Although this is certainly implementable, it violates the natural irreversibility of imperative computation.

The paper "On the Orthogonality of Assignments and Procedures in Algol" by Stephen Weeks and Matthias Felleisen formalizes the orthogonality of the functional (lambda calculus-like) and imperative fragments of an Algol- like language in terms of separate reduction calculi for the two fragments. The essential properties of these are proved independently, and it is also proved that evaluation of a program can be factored into a functional phase, followed by an imperative phase.

The usual basis for specification and verification of programs in simple imperative languages is the familiar "axiomatic" system of [Hoa69 ], based on (precondition, command, postcondition) triples. Unfortunately, most attempts to apply these techniques to languages with full procedures and jumps have been fairly unsatisfactory. The paper "Idealized Algol and its Specification Logic" by John Reynolds, reprinted here as Chapter 6, introduced several innovations:

- specifications as predicates of the environment, with universal specifications those true in all environments;
- logical connectives (conjunction, implication and universal quantification) at the level of specification formulas (i.e., treating Hoare triples as the atomic formulas in a first-order theory);
- "non-interference" predicates to deal with aliasing and interference via non-local variables; and
- call-by-name as the basic parameter mechanism.

One way to highlight unsatisfactory aspects of a model of local variables is to show that it fails to be fully abstract; i.e., fails to validate operationally justified equivalences. The paper "Towards Fully Abstract Semantics for Local Variables" by Albert Meyer and Kurt Sieber, included here as Chapter 7, demonstrates that traditional marked-store models fail to validate some extremely simple expected equivalences. This work also showed the weaknesses of existing program logics, because most logics for imperative languages with procedures were sound in marked-store models, with specification logic being a notable exception.

"The Essence of Algol" was originally presented as an invited address to a symposium in tribute to Adriaan van Wijngaarden, one of the designers of both Algol 60 and Algol 68, on the occasion of his retirement. It is reported that another of the authors of the Algol report commented that Reynolds's paper should have been titled "An Essence of Algol." For comparison, the reader may want to consult some of the other opinions that have been expressed by various authors on what is "essential" about Algol 60 [vW63 , WH66 , Knu67, Str67, Wic73, Hoa74, Cla79, Wex81 , THM83 ], and how it should be formally described [vW64 , Lan64, Mos74, HJ82, THM83 , AW85 ].

The essence of Algol is not a straitjacket. It is a conceptual universe for language design that one hopes will encompass languages far more general than its progenitor.Chapters 8 to 10 explore three language-design possibilities.

"Design of the Programming Language Forsythe" by John Reynolds describes a language based on the ideas presented in "The Essence of Algol." It contains one further innovation: The use of "intersection" (conjunctive) types [CD78 ] to further simplify, unify and generalize the type structure of the language.

"Assignments for Applicative Languages" by Uday Reddy, Vipin Swarup and Evan Ireland, presents an approach to combining imperative and functional aspects by using types to separate imperative and applicative parts of a program. Types are used to keep the procedure mechanism independent of side effects, which allows beta, eta, and other properties of functional languages to be retained. This Algol-like use of types to constrain the scope of effects is at the root of a body of more recent work on introducing assignment into "pure" functional languages [PW93 , LP95].

We have mentioned that, despite being imperative, Algol-like languages preserve all of the reasoning principles used in "pure" functional programming. However, this does not mean that Algol-like languages are necessarily simple to reason about, since this only involves the easy part: reasoning about parts of programs that don't involve change. In particular, it is evident from the examples of specification logic in use in [Rey81] that manipulating non-interference predicates within a logic for program verification is extremely inconvenient. The underlying problem is that interactions between assignments and procedures in conventional higher-order procedural languages can produce undesirable phenomena such as aliasing and covert interference via non-local variables. For this reason, many researchers [Bac78, WA85 , BW88, Hug89, Hud89] abandoned procedural languages entirely and promoted "purely" functional languages in which there is no interference at all. Other language designers have attempted to avoid these problems by significantly circumscribing the procedures in their languages; see, for example, the discussion of Euclid in [Mor82 ].

The paper "Syntactic Control of Interference" by John Reynolds, reprinted here as Chapter 10, demonstrates that it is possible to avoid aliasing and covert interference while retaining Algol-like higher-order procedures in a slightly restricted form. The resulting programming language has not only the desirable functional attributes of Algol 60, but also many of the desirable attributes of simple imperative languages that are typically lost when procedures are added.

Two main strands emerge. The more developed is the explicit-state approach, where programs are modelled using functions that pass states around as values. This approach identifies uniformity properties (based on naturality and relational parametricity) that constrain the way that state is used, analogous to how monotonicity and continuity constrain the way that higher-order functions work in domain theory. Applications include soundness of a program logic and a type system, structuring and design of a translation to intermediate code, and discovery of new reasoning principles.

The other strand is the implicit-state approach, where a program is viewed in terms of a history of observable actions instead of in terms of state transformations. This approach is more recent; it promises to give a very different and complementary way of specifying meanings of imperative programs, and excellent results have been obtained, indicating its potential.

The term "stack discipline" refers to a way of managing the allocation and de-allocation of storage variables at runtime. Reynolds regarded the stack discipline as so integral to Algol's essence that (a mathematical abstraction of) it deserves a prominent position in a satisfactory semantic definition. He shows this viewpoint at work in "Using Functor Categories to Generate Intermediate Code," included as Chapter 12. Phrases in an Algol-like language are translated to intermediate code using the compositionally-defined valuation function for interpretation in a functor category. The semantics is tuned to compiling (instead of input-output behaviour), with store shapes replaced by a category of concrete "stack descriptors" and primitive types interpreted using programs in the intermediate language instead of functions on states.

While Algol's stack discipline was the original focus of functor-category semantics, the ideas have been used also to model dynamic allocation [PS93, Sta96a] and local names in the pi-calculus [Sta96b, FMS96]. In both of these cases a name or location can survive past execution of the block in which it was created: the shape of the store or active name-space is not preserved. Thus, the stack discipline is not built into functor categories themselves, but rather has to do with the specific way that Reynolds and Oles used functors in the semantics of Algol. The point is that a functor-category model can make it clear, in the semantics of types, whether and where it is possible for store shapes to be altered.

The paper "Semantical Analysis of Specification Logic" by Bob Tennent, reprinted here as Chapter 13, addresses this problem by slightly adapting the functor-category approach of Chapters 3 and 11 to allow the treatment of certain "intensional" properties of commands within a formally extensional intuitionistic first-order theory. It turns out that specification logic is incompatible with the law of the excluded middle, and so the use of an underlying intuitionistic logic is not only natural, because of the underlying functor model, but in a sense necessary.

While Chapter 13 solves the previously known problems in the interpretation of specification logic, it also points out an additional problem with the treatment of non-interference predicates in Chapter 6 and [Rey81]: non-interference for procedural phrases is not correctly defined by induction on types as a "logical" predicate. The paper "Semantical Analysis of Specification Logic, 2" by Peter O'Hearn and Bob Tennent, reprinted here as Chapter 14, addresses this problem. It gives a type-independent interpretation of non-interference which, for phrases of basic types, reduces to the definition given in Chapter 13. This interpretation validates all of the axioms for reasoning about non-interference.

These two papers also contain a semantic analysis of passivity, i.e., the ability to read from, but not write to, the store. In Chapter 13 it is shown that expression meanings cannot have side effects, not even "temporary" ones as in the snap-back form of block expression; this is crucial to allow validation of a Hoare-like axiom for assignments in an Algol-like language. This notion of passivity is extended to all types in Chapter 14, again by using a uniform, type-independent, definition.

Specification logic has evolved somewhat with the development of its semantics. Today we regard its essence as consisting of four parts. First, specification logic is a theory, in the negative fragment (universal quantification, conjunction, implication, falsity) of many-sorted first-order intuitionistic logic with equality. The atomic formulas of the theory are Hoare triples {P}C{Q} and non-interference formulas C # E (for arbitrary C and E). Second, the treatment of functional features is LCF-like, with beta/eta-equality, formal function extensionality, and laws for fixed-point unwinding (and induction). Third, for non-interference we have the decomposition schema and axioms for passivity and chastity, as in Chapter 14, and the axioms of strong constancy and non-interference composition. And finally there are analogues of Hoare's axioms for imperative constructs such as sequential composition and iteration, axioms for precedent strengthening, consequent weakening, and so on. Most distinctive is the axiom for variable declarations, which extends the usual Hoare-logic rule by using noninterference assumptions between local variables and non-local identifiers.

Peter O'Hearn and Bob Tennent also use logical relations to construct a model in Chapter 16. They base their construction on the functor-category model of Oles, adding to it relational conditions that govern interactions with local variables. Although their semantic technology is similar to Sieber's, the emphasis is rather different. Where Sieber views relations as a means to "keep a model small," O'Hearn and Tennent view relations as a rigorous approximation to an informal notion of parametricity, as support for a conceptual connection with representation independence and data abstraction [Rey83]. The basic idea is that the information-hiding provided by local variables and procedural abstraction is analogous to the independence of a program using an abstract data type from the details of the implementation of the type; see also [Ten94 ].

Chapter 17, by Andy Pitts, differs from other papers in this volume in that it concentrates on operational rather than denotational methods. Pitts shows how relational-parametricity principles, as in the semantics of Chapter 16 and [OR96 ], can be formulated without explicit reference to a semantic model. He defines logical relations for Idealized Algol based on an operational semantics, and uses these to derive a completeness result characterizing observational equivalence. A main point of his work is that the separation of the reasoning principles implicit in models based on logical relations from their use in constructing the models. This results in a clear and mathematically simple presentation of the resulting principles, and pleasant technical results.

The development of the material in Chapter 18 was done partly in reaction to a paper by Uday Reddy [Red94 ] which, it turns out, provided the first model for the type rules for passivity. Only later it was realized that the treatment of passivity in Chapters 13 and 14 also provides such a model. Reddy sets out his approach in detail in "Global State Considered Unnecessary," reprinted here as Chapter 19.

Reddy's paper is remarkable in a number of respects. First, it is an implicit state semantics, in that imperative programs are treated in terms of sequences of observable actions, instead of as transformations on a set of states. (This it has in common with ideas from the process-calculus literature [Mil89].) At the same time the semantics is domain-theoretic, in much the same spirit as domain models of functional languages. This allows suitable categorical structure to be identified, resulting in a novel semantics of syntactic control of interference.

The second remarkable aspect of Reddy's paper is that it contains the first semantic account of the irreversibility of state change in imperative programs. The idea at issue is expressed by Strachey in Chapter 2 of Volume 1 as follows:

The machine state behaves in a typically "operational" way. The state transformation produced by obeying a command is essentially irreversible and it is, by the nature of the computers we use, impossible to have more than one version of [the state] available at any one time.The problem is that previous models contain "snapback" operators which contradict this idea of irreversibility. (A treatment of irreversibility has recently been obtained in an explicit-state setup as well [OR96 ], using a linear form of parametricity to exclude snap-back operators.)

While Reddy's model accounts nicely for local state and irreversibility, it does not treat interference as well. That is, non-interference seems to be built into the treatment of procedures, so a semantics of syntactic control of interference can be given, but not full Idealized Algol. This was partially resolved in [OR95 ] by embedding the model into a functor category but, though the semantics has good theoretical properties, the model construction is rather technical and ad hoc in comparison to both Reddy's basic model and other functor-category models.

In "Linearity, Sharing and State," reprinted here as Chapter 20, Samson Abramsky and Guy McCusker use the framework of game semantics to formulate an implicit-state model for full Idealized Algol (with side effects in expressions). Their model construction is striking; it extends the semantics of the functional language PCF developed by Martin Hyland and Luke Ong [HO94 ] by simply dropping the "innocence" condition (innocence is a game-theoretic expression of functional behaviour). Programs denote strategies for playing a game, and as such may be sensitive to a whole history of events (or "prior moves"): non-innocent access to the history corresponds to imperative, implicitly stateful, behaviour. It is shown that all "compact" strategies in the model are definable in the language, and after quotienting, this results in a fully abstract model.

The game model exemplifies Abramsky's general theme of "composition as parallel composition plus hiding" [Abr93, Abr94]. It is interesting to revisit Reddy's work in light of this. Reddy also emphasized the parallel nature of composition or application, but focused on what might be thought of as a "true-concurrency" or "independent-composition" view of parallelism. This is what, it appears, stopped him from accounting for interference between procedure and argument in a determinate fashion. In contrast, the parallelism in the game model is more reminiscent of coroutines (and as such harkens back to [BC82 ]), with a single thread of control jumping back and forth between procedure and argument. This allows interference to be handled quite naturally in a way that maintains determinacy.

Up to this point the focus has been on sequential versions of Algol. The question arises as to whether all of this development is dependent on the sequential nature of the languages studied, or, rather, what parts of it can extend smoothly to concurrency. Steve Brookes addresses this question in Chapter 21. He formulates a functor-category model for a parallel version of Idealized Algol; the use of a functor category shows that the shape of the store is the same in the initial and final states in the evaluation of any command. In a parallel language this does not imply that allocation is truly stack-like if two threads are interleaved on a single processor, but it does establish invariants for the allocator. The semantics of parallel features is then a straightforward extension of one previously given for a parallel language without procedures [Bro93], with care taken to account for appropriate naturality conditions. Brookes regards the integration of this semantics with the treatment of procedures and storage allocation given by functor categories as evidence for the orthogonality of procedures and parallelism in Algol-like languages.

P. W. O'Hearn and R. D. Tennent

September, 1996.