Separation Logic has witnessed tremendous success in recent years in reasoning about programs that deal with heap storage. Its success owes to the fundamental principle that one should keep separate areas of the heap storage separate in program reasoning. However, the way Separation Logic deals with program variables continues to be based on traditional Hoare Logic without taking any benefit of the separation principle. This has led to unwieldy proof rules suffering from lack of clarity as well as questions surrounding their soundness. In this paper, we extend the separation idea to the treatment of variables in Separation Logic, especially Concurrent Separation Logic, using the system of Syntactic Control of Interference proposed by Reynolds in 1978. We extend the original system with permission algebras, making it more powerful and able to deal with the issues of concurrent programs. The result is a streamined presentation of Concurrent Separation Logic, whose rules are memorable and soundness obvious. We also include a discussion of how the new rules impact the semantics and devise static analysis techniques to infer the required permissions automatically.

To verify program specifications, rather than generic safety properties, it will be necessary to integrate verification into the process of programming. Program proving is unlike theorem proving in mathematics mathematical conjectures may give no hint as to how they could be proved, but programs are written by programmers, who must understand informally why their programs work. The job of verification is not to explore some immense search space, but to formalize the programmer's intuitions until any faults are revealed. This requires specifications and proofs that are succinct and intelligible which in turn require logics that go be yond predicate calculus (the assembly language of program proving). In this talk, I will recount and illustrate several steps, old and new, towards this goal - particularly in the treatment of arrays.

We investigate proof rules for information hiding, using the formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from those accessed by the module's clients. The use of a logical connective gives rise to a form of dynamic partitioning, where we track the transfer of ownership of portions of heap storage between program components. It also enables us to enforce separation in the presence of mutable data structures with embedded addresses that may be aliased.

We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We state semantically what is meant by correctness of a copying garbage collector, and employ a variant of the novel separation logics to formally specify partial correctness of Cheney's copying garbage collector in our program logic. Finally, we prove that our implementation of Cheney's algorithm meets its specification using the logic we have given and auxiliary variables.

We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We then state what is meant by correctness of a copying garbage collector, and employ a variant of the novel separation logics [18, 23] to formally specify partial correctness of Cheney's copying garbage collector [8]. Finally, we prove that our implementation of Cheney's algorithm meets its specification, using the logic we have given, and auxiliary variables [19].

We investigate proof rules for information hiding, using the recent formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from those accessed by the module's clients. The use of a logical connective gives rise to a form of dynamic partitioning, where we track the transfer of ownership of portions of heap storage between program components. It also enables us to enforce separation in the presence of mutable data structures with embedded addresses that may be aliased.

In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure. The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a "separating conjunction" that asserts that its subformulas hold for disjoint parts of the heap, and a closely related "separating implication". Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing. In this paper, we survey the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. We also discuss promising future directions.

In a linearly-typed functional language, one can define functions that consume their arguments in the process of computing their results. This is reminiscent of state transformations in imperative languages, where execition of an assignment statement alters the contents of the store. We explore this connection by translating two variations on Algol 60 into a purely functional language with polymorphic linear types. On the one hand, the translations lead to a semantic analysis of Algol-like programs, in terms of a model of the linear language. On the other hand, they demonstrate that a linearly-typed functional language can be at least as expressive as Algol.

In the early 80's Oles and Reynolds devised a semantic model of Algol-like languages using a category of functors from a category of store shapes to the category of predomains. Here we will show how a variant of this idea can be used to define the translation of an Algol-like language to intermediate code in a uniform way that avoids unnecessary temporary variables, provides control-flow translation of boolean expressions, permits online expansion of procedures, and minimizes the storage overhead of calls of closed procedures. The basic idea is to replace continuations by instruction sequences and store shapes by descriptions of the structure of the run-time stack.

No abstract available.

In programming languages which permit both assignment and procedures, distinct identifiers can represent data structures which share storage or procedures with interfering side effects. In addition to being a direct source of programming errors, this phenomenon, which we call interference can impact type structure and parallelism. We show how to eliminate these difficulties by imposing syntactic restrictions, without prohibiting the kind of constructive interference which occurs with higher-order procedures or SIMULA classes. The basic idea is to prohibit interference between identifiers, but to permit interference among components of collections named by single identifiers.

A domain of flow diagrams similar to that proposed by Scott, a domain of linear flow diagrams proposed by Goguen et al , a domain of decision table diagrams involving mfimtary branching, and a domain of processes based on the ideas of Milner and Beklc are each provided with a direct semantics, closely related to partial-function semantics, and a continuation semantics similar to that developed by Morris and Wadsworth It is shown that there is a variety of meaning-preserving continuous functions among these language-hke domains, that every direct semantics possesses an "equivalent" continuation semantics, and that there is a particular continuation semantics which always gives distinct meanings to distinct processes The proofs utilize the algebraic methods of Goguen et al , which are extended to continuous algebras with operations whose arguments can be Indexed by mflmte sets or even domains.