1 July - 31 December 1995
Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)
The object of this short workshop is to stimulate discussion of the top-down approach to semantics for system design. The format will be highly informal. The idea is to stimulate more intimate discussions between those experienced in a variety of semantic approaches. For this reason, the emphasis will be on challenges, open questions, and work in progress, rather than background, results or conclusions.
A tutorial on relations and predicate transformers: Clare Martin
This talk will discuss both the established results and outstanding challenges associated with the uniform algebraic construction of relations and predicate transformers. The established results include a complete rule for data refinement, some new refinement rules, and some laws which could lead to a typed version of a programming formalism known as the refinement calculus. The outstanding challenges fall into two categories: some concern the rigorous mathematical foundations of this construction of predicate transformers, and others concern its application to different programming formalisms. It is hoped that the presentation of these challenges to a new audience might yield some fresh insights into this subject.
From Algebra to Operational Semantics: He Jifeng
Approaches to programming semantics may be broadly classified as specification-oriented, algebraic, and operational. It is the goal of theoretical research to link the three styles of presentation by mathematical calculation or proof. The choice of starting point is optional: it is customary to start with operational semantics, choose one of a variety of bisimulations, and deduce a range of algebraic theories at varying levels of abstraction. In this lecture, we reverse the traditional direction. Starting with an algebraic semantics of sufficient power, it is possible to choose one of a variety of implementation strategies, and then derive the details of an operational semantics by algebraic calculation. The same techniques may be applicable to development of provably correct compilers.
Power simulation is the weakest reasonable precongruence: Paul Gardiner
Power simulation is a simuation between powersets. In sequential programming, a collection of operations may be validly replaced in all contexts by another collection if there is a power simulation between hem. The result is extended to process algebra, with a demonstration that power similarity is the weakest compositional ordering that distinguishes the possibility of deadlock.
Transformer semantics and higher order programs: David Naumann
Highlights of a predicate transformer semantics for a higher order imperative language will be given. The language includes stored procedures that can have global variables. In order to obtain a simple-minded semantics and sidestep difficult problems in the semantics of Algol-like languages, we impose restrictions on global variables. Implications for language design will be discussed. The semantics lives in one of Martin's skew span categories.
Unifying Theories of Programming: Tony Hoare
Unification of theories is the long-standing goal of the natural sciences; and modern physics offers a spectacular paradigm of its achievement. The structure of modern mathematics has also been determined by its great unifying theories - topology, algebra and the like. The same ideals and goals are shared by students of theoretical computing science.