Date: Thu, 13 Dec 2001 15:27:49 -0800 From: Christine Sosa <sosacsli.stanford.edu> Subject: Semantics: A Paradigm for Program Semantics
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 page
CSLI Publications 2001.
http://cslipublications.stanford.edu , email: pubscsli.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.
Pubs-postscript-html
-----------------
Major Supporters ----------------