Announcing: A PARADIGM FOR PROGRAM SEMANTICS

[Christine Sosa]

CSLI Publications is pleased to announce the availability of:

A PARADIGM FOR PROGRAM SEMANTICS: POWER STRUCTURES AND DUALITY: Chris
Brink (University of Wollongong and Ingrid Rewitzky (University of
Cape Town); paper ISBN: 1-57586-344-8, $27.50, cloth ISBN:
1-57586-345-6, $67.50, 284 pages. CSLI Publications 2001.
http://cslipublications.stanford.edu , email: pubs at csli.stanford.edu.

To order this book, contact The University of Chicago Press. Call
their toll free order number 1-800-621-2736  (U.S. & Canada only)  or
order online at http://www.press.uchicago.edu/ (use the search
feature to locate the book, then order).

Book description:
This book provides a synthesis of four versions of program semantics.
In relational semantics a program is thought of as a binary
input-output relation over some state space; in predicate transformer
semantics a program is a mapping from predicates to predicates; in
information systems (and Hoare logic) a program is considered as a
relation between predicates; and in domain theory a program is a
multifunction mapping states to sets of states. Brink and Rewitzky
show, through an exhaustive case study analysis, that it is possible
to do back-and-forth translation from any of these versions of
program semantics from and to any of the others. They do so by
invoking techniques from non-classical logics, lattice theory,
topology and the calculus of binary relations. At the heart of their
method is the notion of a power construction along with an invocation
of duality theory. A power construction lifts a given structure from
its base set to its power set (the set of all its subsets); duality
theory is then used to  recapture the original structure from the
lifted structure. Specifcally, the duality theory at work in this
book is Priestley duality, which identifies certain topological
spaces (Priestley spaces) as the duals of bounded distributive
lattices. In the authors' version, relational Priestley spaces are
the duals of bounded distributive lattices with operators.
The importance of this book lies in its demonstration that, although
there are many variations of each of the four versions of program
semantics, in principle they may be thought of as intertranslatable.