Algol-like languages, languages of great theoretical and practical importance, are studied in this paper. Following the stance that procedures act on the state that exists at their point of declaration, and that a variable (associated with an active integer) can be modeled as a side-effect and a value, effectively allowing value-returning commands, the authors address the concepts of locality and state-change irreversibility, history being implicit within a state, so that earlier states cannot be retrieved.

The constructions follow from the object-based approach of Reddy and the categorical approach of Reynolds, and involve a great deal of category theory. Beginning with coherent spaces (sequences of operations on which a consistency relation is defined), Algol commands are modeled as regular maps. These preserve (in-)consistency and are “history free.” Declaring a new variable causes the current store shape to be enlarged, giving a new shape (a “product”) on which subsequent commands act. Using a standard construction due to Yoneda, products are preserved under embedding, and this ultimately leads to an implementation of sharing that allows interference via the determinate use of interfering objects in a shared evaluation context. This is well described as “active sequentiality.”

Throughout, the authors provide a helpful dialogue, explaining their motivations and aspirations, as well as their reservations. The paper concludes with a full abstraction result that further strengthens the “decoupling” of the meaning of a procedure from its “internal data.” Apart from the references mentioned in the paper, similar, related material can be found in O’Hearn and Reynolds [1].