Metric semantics for concurrency

An overview is given of work we have done in recent years on the semantics of concurrency, concentrating on semantic models built on metric structures. Three contrasting themes are discussed, viz. (i) uniform or schematic versus nonuniform or interpreted languages; (ii) operational versus denotational semantics, and (iii) linear time versus branching time models. The operational models are based on Plotkin's transition systems. Language constructs which receive particular attention are recursion and merge, synchronization and global nondeterminacy, process creation, and communication with value passing. Various semantic equivalence results are established. Both in the definitions and in the derivation of these equivalences, essential use is made of Banach's theorem for contracting functions.Dedicated to Peter Naur on the occasion of his 60th birthday