Algol-like Languages, Introduction


Introduction to Volume 1
Part I Historical Background
Part II Basic Principles
Part III Language Design
Introduction to Volume 2
Part IV Functor-Category Semantics
Part V Specification Logic
Part VI Procedures and Local Variables
Part VII Interference, Irreversibility and Concurrency
Acknowledgements
Bibliography


Introduction to Volume 1

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.

Part I Historical Background

In 1959, John Backus presented a paper [Bac59] on "the proposed international algebraic language" (which soon after evolved into the language that became known as Algol 60 [NB#60]). Backus begins by giving informal descriptions of the syntax and semantics of the language, and outlines reasons why more precise descriptions are needed. But he then makes the following admission.
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].

Part II Basic Principles

A significant change in attitudes to Algol 60was initiated by the paper "The Essence of Algol" by John Reynolds, reprinted here as Chapter 3. At the time (1981), this language was generally regarded as having been superseded by new and improved "Algol-like" languages, such as Algol 68 [vW#69 ] and Pascal [Wir71]. But Reynolds argues that such languages are not truly Algol 60-like, and, in many important respects, are less satisfactory than the original. This is reminiscent of Tony Hoare's opinion [Hoa74 ] that Algol 60is
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.

  1. 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.
  2. The language has assignments, but procedures, variables, and other denotable meanings are not assignable.
  3. Apart from overflow, roundoff error, and error stops, expressions are purely "mathematical," without non-local jumps, side effects, or ambiguous coercions.
  4. Allocation and de-allocation are based on a stack discipline, but the treatment of storage variables is otherwise representation independent.
  5. Generic features such as conditionals, recursion, and procedures are uniformly applicable to all types of phrases.
According to these criteria, languages such as Algol 68 and Pascal and their descendants are not Algol-like. (In some minor respects, such as the incomplete typing for parameters, even Algol 60 is not Algol-like! but these are regarded as design mistakes.)

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:

Specification logic may be viewed as a combination of Hoare's logic and Scott's "Logic of Computable Functions" [Sco69], in the same way that Idealized Algol combines a simple imperative language with a PCF-like typed lambda calculus. Examples of specification logic in use may be found in Section 3.3 of [Rey81], where a subset of Algol W is used as the programming language.

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

Part III Language Design

Reynolds concludes "The Essence of Algol" with the following remarks.
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.

Introduction to Volume 2

In this volume, Algol-like languages are studied from various modern denotational-semantic points of view. This material will be suitable for advanced seminars and researchers with adequate background in logic, domain theory, type theory and category theory.

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.

Part IV Functor-Category Semantics

The functor-category approach to the semantics of local variables outlined in "The essence of Algol" is described in detail in Frank Oles's Ph.D. thesis. Excerpts from this work have been included here as Chapter 11; see also [Ole85, OT92]. This chapter describes how the extension of the store via local variable declarations can be represented using a category of store shapes and expansions, and how a treatment of procedures consistent with this view of local declarations can be obtained using a category of functors from store shapes into domains.

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.

Part V Specification Logic

In Chapters 6 and 10, Reynolds focused on non-interference as a means of controlling and reasoning about interactions between procedures and imperative features. But the semantics of non-interference has proved to be rather subtle. An operational semantics of specification logic is sketched in [Rey81], but the final section of Chapter 6 points out that this interpretation is not completely satisfactory. In particular, it fails to validate two powerful, and seemingly reasonable, axioms that make use of non-interference assumptions.

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.

Part VI Procedures and Local Variables

In Chapter 7 of Volume 1, Meyer and Sieber emphasized that traditional denotational models of imperative languages fail to capture the sense in which non-local procedures are independent of locally-declared variables. An "invariant-preserving" model described in that paper accounts for some of the difficulties, and this line of work is continued by Kurt Sieber in Chapter 15. Sieber uses the concept of "logical relations" [Plo73, Sta85] as a means to exclude undesirable elements. A full-abstraction result is given showing the coincidence of semantic equality and a contextually-defined "observational" equivalence relation, up to second-order types.

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.

Part VII Interference, Irreversibility and Concurrency

In "Syntactic Control of Interference" (Chapter 10 of Volume 1) Reynolds argues that a language should be constrained to make non-interference easily detectable. The language design given there is very successful in most respects; but it is pointed out that the treatment of passivity is such that syntactic correctness is not always preserved by fi-reductions. This problem has since been addressed by Reynolds in [Rey89]. A somewhat simpler solution to the problem is presented in "Syntactic Control of Interference Revisited" by Peter O'Hearn, John Power, Makoto Takeyama and Bob Tennent, reprinted here as Chapter 18.

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.

Acknowledgements

We are very grateful to all of the contributors for their cooperation in producing these volumes, to Robin Milner for supporting this project to Birkh"auser, to Edwin Beschler of Birkh"auser for his confidence in us, to Lockwood Morris for proofreading, to Elaine Weinman for TEXnical typing, and to John Jorgensen for assistance in setting up our fonts.

P. W. O'Hearn and R. D. Tennent
September, 1996.

Bibliography

  • [Abr93] S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111(1-2):3-57, April 12 1993.
  • [Abr94] S. Abramsky. Interaction categories and communicating sequential processes. In Roscoe [Ros94], chapter 1, pages 1-16.
  • [AW85] S. K. Abdali and D. S. Wise. Standard, storeless semantics for Algol-style block structure and call-by-name. In A. Melton, editor, Mathematical Foundations of Programming Semantics, volume 239 of Lecture Notes in Computer Science, pages 1-19, Manhattan, Kansas, April 1985. Springer-Verlag, Berlin (1986).
  • [Bac59] J. W. Backus. The syntax and semantics of the proposed international algebraic language of the Zurich ACM -GAMM Conference. In Information Processing, Proceedings of the International Conference on Information Processing, pages 125-131, Paris, June 1959.
  • [Bac78] J. Backus. Can programming be liberated from the von Neumann style? a functional style and its algebra of programs. Comm. ACM, 21(8):613-641, August 1978.
  • [BC82] G. Berry and P-L. Curien. Sequential algorithms on concrete data structures. Theoretical Computer Science, 20:265-321, 1982.
  • [Bro93] S. Brookes. Full abstraction for a shared variable parallel language. In Proceedings, 8th Annual IEEE Symposium on Logic in Computer Science, pages 98-109, Montreal, Canada, 1993. IEEE Computer Society Press, Los Alamitos, California.
  • [Bur70] R. M. Burstall. Formal description of program structure and semantics in first-order logic. In B. Meltzer and D. Michie, editors, Machine Intelligence 5, pages 79-98. Edinburgh University Press, Edinburgh, 1970.
  • [BW88] R. Bird and P. Wadler. Introduction to Functional Programming. Prentice-Hall International, London, 1988.
  • [CD78] M. Coppo and M. Dezani. A new type assignment for lambda-terms. Archiv. Math. Logik, 19:139-156, 1978.
  • [Chu41] A. Church. The Calculi of Lambda Conversion. Princeton University Press, Princeton, 1941.
  • [Cla79] E. M. Clarke. Programming language constructs for which it is impossible to obtain good Hoare-like axiom systems. J. ACM, 26(1):129-147, 1979.
  • [DHW76] R. M. De Morgan, I. D. Hill, and B. A. Wichmann. A supplement to the Algol 60 Revised Report. The Computer Journal, 19(3):276-288, 1976.
  • [FMS96] M. Fiore, E. Moggi, and D. Sangiorgi. A fully abstract model for the pi-calculus. In [LIC96], pages 43-54.
  • [HJ82] W. Henhapl and C. B. Jones. Algol 60. In D. Bjorner and C. B. Jones, editors, Formal Specification and Software Development, pages 141-173. Prentice-Hall International, London, 1982.
  • [HJ89] C. A. R. Hoare and C. B. Jones, editors. Essays in Computing Science. Prentice Hall International, 1989.
  • [HO94] J. M. E. Hyland and C.-H. L. Ong. On full abstraction for PCF: I, II and III. Submitted for publication, 1994.
  • [Hoa69] C. A. R. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12(10):576-580 and 583, 1969.
  • [Hoa74] C. A. R. Hoare. Hints on programming-language design. In C. Bunyan, editor, Pages 193-216 of [HJ89].
  • [Hud89] P. Hudak. Conception, evolution, and application of functional programming languages. Computing Surveys, 31:359-411, 1989.
  • [Hug89] J. Hughes. Why functional programming matters. The Computer Journal, 32:98-107, 1989.
  • [Knu67] D. E. Knuth. The remaining troublespots in Algol 60. Comm. ACM, 10(10):611-617, 1967.
  • [Lan64] P. J. Landin. A formal description of Algol 60. In Steel [Ste64], pages 266-294.
  • [Lan65] P. J. Landin. A correspondence between Algol 60 and Church's lambda notation. Comm. ACM, 8(2,3):89-101 and 158-165, 1965.
  • [LIC96] Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Jersey, USA, 1996. IEEE Computer Society Press, Los Alamitos, California.
  • [LP95] J. Launchbury and S. Peyton Jones. State in Haskell. Lisp and Symbolic Computation, 8(4):293-341, December 1995.
  • [Mil89] R. Milner. Communication and Concurrency. Prentice-Hall International, 1989.
  • [Mor82] J. H. Morris. Real programming in functional languages. In J. Darlington, P. Henderson, and D. A. Turner, editors, Functional Programming and its Applications, pages 129-176. Cambridge University Press, Cambridge, England, 1982.
  • [Mos74] P. Mosses. The mathematical semantics of Algol 60. Technical monograph PRG-12, Oxford University Computing Laboratory, Programming Research Group, Oxford, January 1974.
  • [MS76] R. E. Milne and C. Strachey. A Theory of Programming Language Semantics. Chapman and Hall, London, and Wiley, New York, 1976.
  • [NB#60] P. Naur (ed.), J. W. Backus, et al. Report on the algorithmic language Algol 60. Comm. ACM, 3(5):299-314, 1960. Also Numerische Mathematik 2:106-136.
  • [NB#63] P. Naur, J. W. Backus, et al. Revised report on the algorithmic language Algol 60. Comm. ACM, 6(1):1-17, 1963. Also The Computer Journal 5:349-67, and Numerische Mathematik 4:420-53.
  • [Ole85] F. J. Oles. Type algebras, functor categories and block structure. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, pages 543-573. Cambridge University Press, Cambridge, England, 1985.
  • [OR95] P. W. O'Hearn and U. S. Reddy. Objects, interference, and the Yoneda embedding. In S. Brookes, M. Main, A. Melton, and M. Mislove, editors, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference, volume 1 of Electronic Notes in Theoretical Computer Science, Tulane University, New Orleans, Louisiana, March 29-April 1 1995. Elsevier Science (http://www.elsevier.nl).
  • [OR96] P. W. O'Hearn and J. C. Reynolds. From Algol to polymorphic linear lambda-calculus. Unpublished draft, 1996.
  • [OT92] P. W. O'Hearn and R. D. Tennent. Semantics of local variables. In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Applications of Categories in Computer Science, volume 177 of London Mathematical Society Lecture Note Series, pages 217-238. Cambridge University Press, Cambridge, England, 1992.
  • [Plo73] G. D. Plotkin. Lambda-definability and logical relations. Memorandum SAI RM-4, School of Artificial Intelligence, University of Edinburgh, October 1973.
  • [PS93] A. Pitts and I. Stark. Observable properties of higher order functions that dynamically create local names, or: What's new? In A. M. Borzyszkowski and S. Sokolowski, editors, Mathematical Foundations of Computer Science, volume 711 of Lecture Notes in Computer Science, pages 122-140, Gdansk, Poland, 1993. Springer-Verlag, Berlin.
  • [PW93] S. Peyton-Jones and P. Wadler. Imperative functional programming. In Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 71-84, Charleston, South Carolina, 1993. ACM, New York.
  • [Red94] U. S. Reddy. Passivity and independence. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 342-352, Paris, France, 1994. IEEE Computer Society Press, Los Alamitos, California.
  • [Rey81] J. C. Reynolds. The Craft of Programming. Prentice-Hall International, London, 1981.
  • [Rey83] J. C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513-523, Paris, France, 1983. North-Holland, Amsterdam.
  • [Rey89] J. C. Reynolds. Syntactic control of interference, part 2. In G. Ausiello, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca, editors, Automata, Lan guages and Programming, 16th International Colloquium, volume 372 of Lecture Notes in Computer Science, pages 704-722, Stresa, Italy, July 1989. Springer-Verlag, Berlin.
  • [Rey93] J. C. Reynolds. The discoveries of continuations. Lisp and Symbolic Compu tation, 6(3/4):233-247, 1993.
  • [Ros94] A. W. Roscoe, editor. A Classical Mind, Essays in Honour of C. A. R. Hoare. Prentice-Hall International, 1994.
  • [Sco69] D. S. Scott. A type-theoretical alternative to Cuch, Iswim, Owhy. Privately circulated memo, Oxford University, October 1969. Published in Theoretical Computer Science, 121(1/2):411-440, 1993.
  • [Sco72a]D. S. Scott. Mathematical concepts in programming language semantics. In Proc. 1972 Spring Joint Computer Conference, pages 225-34. AFIPS Press, Montvale, N.J., 1972.
  • [Sco72b]D. S. Scott. Models for various type-free calculi. In P. Suppes et al., edi tors, Logic, Methodology, and the Philosophy of Science, IV, pages 157-187, Bucharest, 1972. North-Holland, Amsterdam.
  • [SS71] D. S. Scott and C. Strachey. Toward a mathematical semantics for computer languages. In J. Fox, editor, Proceedings of the Symposium on Computers and Automata, volume 21 of Microwave Research Institute Symposia Series, pages 19-46. Polytechnic Institute of Brooklyn Press, New York, 1971. Also Technical Monograph PRG-6, Oxford University Computing Laboratory, Programming Research Group, Oxford.
  • [Sta85] R. Statman. Logical relations and the typed lambda-calculus. Information and Computation, 65:85-97, 1985.
  • [Sta96a]I. Stark. Categorical models for local names. Lisp and Symbolic Computation, 9(1):77-107, feb 1996.
  • [Sta96b]I.A. Stark. A fully abstract domain model for the pi-calculus. In [LIC96], pages 36-42.
  • [Ste64] T. B. Steel, Jr., editor. Formal Language Description Languages for Com- puter Programming, Proceedings of the IFIP Working Conference, Baden bei Wien, Austria, September 1964. North-Holland, Amsterdam (1966).
  • [Sto77] J. E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Pro- gramming Language Theory. The MIT Press, Cambridge, Massachusetts, and London, England, 1977.
  • [Str67] C. Strachey. Fundamental Concepts in Programming Languages. Unpublished lecture notes, International Summer School in Computer Programming, Copenhagen, August 1967.
  • [SW74] C. Strachey and C. P. Wadsworth. Continuations: a mathematical semantics for handling full jumps. Technical Monograph PRG-6, Oxford University Computing Laboratory, Programming Research Group, Oxford, 1974.
  • [Ten94] R. D. Tennent. Correctness of data representations in Algol-like languages. In Roscoe [Ros94], chapter 23, pages 405-417.
  • [THM83] B. A. Trakhtenbrot, J. Y. Halpern, and A. R. Meyer. From denotational to operational and axiomatic semantics for Algol-like languages: an overview. In E. M. Clarke, Jr. and D. Kozen, editors, Logics of Programs 1983, volume 164 of Lecture Notes in Computer Science, pages 474-500, Pittsburgh, PA, 1983. Springer-Verlag, Berlin, 1984.
  • [vW63] A. van Wijngaarden. Generalized Algol. In R. Goodman, editor, Annual Review in Automatic Programming, volume 3, pages 17-26. Pergamon Press, Oxford, 1963.
  • [vW64] A. van Wijngaarden. Recursive definition of syntax and semantics. In Steel [Ste64], pages 13-24.
  • [vW#69] A. van Wijngaarden (ed.) et al. Report on the algorithmic language Algol 68. Numerische Mathematik, 14:79-218, 1969.
  • [WA85] W. W. Wadge and E. A. Ashcroft. Lucid, the Dataflow Programming Language, volume 22 of APIC Studies in Data Processing. Academic Press, Lon- don, 1985.
  • [Wex81] R. L. Wexelblat, editor. History of Programming Languages. Academic Pres, New York, 1981.
  • [WH66] N. Wirth and C. A. R. Hoare. A contribution to the development of Algol. Comm. ACM, 9(6):413-432, June 1966.
  • [Wic73] B. A. Wichmann. Algol 60 Compilation and Assessment. Academic Press, London, 1973.
  • [Wir71] N. Wirth. The programming language Pascal. Acta Informatica, 1:35-63, 1971.