A Resumption Monad Transformer and its Applications in the Semantics of Concurrency

Abstract

Resumptions are a valuable tool in the analysis and design of semantic models for concurrent programming languages, in which computations consist of sequences of atomic steps that may be interleaved. In this paper we consider a general notion of resumption, parameterized by the kind of computations that take place in the atomic steps. We define a monad transformer which, given a monad M that represents the atomic computations, constructs a monad R(M) for interleaved computations. Moreover, we use this monad transformer to define the denotational semantics of a simple imperative language supporting nondeterminism and concurrency.