Linear Structures for Concurrency in Probabilistic Programming Languages

We introduce a semantical model based on operator algebras and we show the suitability of this model to capture both a quantitative version of non-determinism (in the form of a probabilistic choice) and concurrency. We present the model by referring to a generic language which generalises various probabilistic concurrent languages from different programming paradigms. We discuss the relation between concurrency and the commutativity of the resulting semantical domain. In particular, we use Gelfand's representation theorem to relate the semantical models of synchronisation-free and fully concurrent versions of the language. A central aspect of the model we present is that it allows for a unified view of both operational and denotational semantics for a concurrent language.