Control Flow Semantics

J. W. de Bakker is Professor at the Centrum voor Wiskinde en Informatica in Amsterdam. Erik de Vink is Professor in the Department of Mathematics and Computer Science at Eindhoven University of Technology.

Part 1 Fundamentals: recursion and iteration - recursion - transition systems and higher-order definitions, interation - a nonuniform language with continuation semantics, exercises, bibliographical notes; nondeterminacy - metric hyperspaces, nondeterministic choice - the compact power-domain, exercises, bibliographical notes; variations - guarded commands - D without higher order, goto statements - systems of continuations, exercises, bibliographical notes. Part 2 Linear models: uniform parallelism - parallel com-position - introduction of "II", process creation - parallel resumptions, exercises, bibliographical notes; unbounded non-determinism - image-finite transition systems - closed replaces compact, random assignment - the closed powerdomain, fair merge - enforcing image-finiteness, exercises, biblio-graphical notes; locality - blocks - environments for in-dividual variables, function procedures with parameters called-by-value - statement and expression prolongations, exercises, bibliographical notes; nonuniform parallelism - parallel composition with shared variables - relating O and D through abstraction, concurrent evaluation of expressions - many sorted transition systems, exercises, bibliographical notes; recursion revisited - the u-calculus Lu-a declaration free formalism, procedure environments -D without higher order, Lcf and Lu compared - simultaneous versus iterated fixed points, three semantics for Lcf - fixed points at different levels, exercises, bibliographical notes; nested resumptions - backtracking - success and failure pro-longations, the fork statement - contractiveness through hiatons, exercises, bibliographical notes. Part 3 Models based on domain equations: domain equations and bisimulation - domain equations, nonexpansive and contractive functors, bisimulation, exercises, bibliographical notes; branching domains at work - deadlock - a branching domain for D, synchronisation - refining the parallel composition, exercises, bibliographical notes; extensions of nonuniform parallelism - suspension and the await statement - a non-uniform domain equation, communication with value passing - a nonuniform version of Lsyn. (Part contents).