An Operational Semantics of First-class Synchronous Operations

Abstract

First-class synchronous operations are a new approach to synchronization and communication in concurrent languages. They have been informally described in [Rep88], and [Rep91a]; this paper presents an operational semantics for an untyped language with first-class synchronous operations. This language in- cludes a large fraction of the concurrency primitives of Concurrent ML CML), a concurrent extension of SML, and is the first step toward formalizing the definition of CML.