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.

- 10.00-10.30 Registration, coffee
- 10.30-11.30 Clare Martin, "Relations and Predicate Transformers"
- 11.30-12.00 Questions and Discussion
- 12.00-14.00 Lunch
- 14.00-15.00 He Jifeng, "From Algebra to Operational Semantics"
- 15.00-15.30 Questions and Discussion
- 15.30-16.00 Tea
- 16.00-17.00 Robert Tennent, "What is Data Refinement?"
- 17.00-17.30 Questions and Discussion

- 10.00-11.00 Paul Gardiner, "Power simulation is the weakest reasonable preconguence"
- 11.00-11.30 Coffee
- 11.30-12.00 Questions and Discussion
- 12.00-14.00 Lunch
- 14.00-15.00 David Naumann, "Transformer semantics and higher order programs"
- 15.00-15.30 Questions and Discussion
- 15.30-16.00 Tea
- 16.00-17.00 C A R Hoare, "Unifying Theories"
- 17.00-17.30 Questions and Discussion

- 9.30-10.30 Panel Discussion. Chair: Cliff Jones
- 10.30-11.00 Coffee
- 11.00-12.00 *open to volunteers*
- 12.00-14.00 Lunch

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