Concurrency Semantics in Continuation-Passing Style

We present a denotational semantics designed in continuation-passing style (CPS) for an abstract language providing operators for nondeterministic choice, sequential and parallel composition, and a general mechanism of interaction between multisets of distributed actions. We show that the basic laws of concurrent systems are satisfied in this semantics. Next, by customizing the behavior of continuations we obtain denotational semantics for a couple of concurrent languages and a nature-inspired formalism. The languages discussed include Hoare's communicating sequential processes (CSP), and two formalisms based on multiparty interactions: a version of CSP extended with communication and synchronization on multiple channels, and a language similar to a process algebra for DNA computing introduced by Cardelli. We accomplish the semantic investigation in the mathematical framework of complete metric spaces.

---

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).