Mixing Metaphors: Actors as Channels and Channels as Actors
Channel- and actor-based programming languages are both used in practice, but the two are often confused. Languages such as Go provide anonymous processes which communicate using buffers or rendezvous points—known as channels—while languages such as Erlang provide addressable processes—known as actors—each with a single incoming message queue.
The lack of a common representation makes it difficult to reason about translations that exist in the folklore. We define a calculus λch for typed asynchronous channels, and a calculus λact for typed actors. We define translations from λact into λch and λch into λact and prove that both are type- and semantics-preserving. We show that our approach accounts for synchronisation and selective receive in actor systems and discuss future extensions to support guarded choice and behavioural types.
Thu 22 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:50 - 17:30 | Calculi and SemanticsECOOP Research Papers at Auditorium, Vertex Building Chair(s): Colin Gordon Drexel University | ||
15:50 25mTalk | Modelling homogeneous generative meta-programming ECOOP Research Papers Link to publication Media Attached | ||
16:15 25mTalk | Mixing Metaphors: Actors as Channels and Channels as Actors ECOOP Research Papers Simon Fowler The University of Edinburgh, Sam Lindley University of Edinburgh, UK, Philip Wadler University of Edinburgh, UK Link to publication Pre-print Media Attached | ||
16:40 25mTalk | μPuppet: A Declarative Subset of the Puppet Configuration Language ECOOP Research Papers Weili Fu University of Edinburgh, Roly Perera University of Edinburgh, UK / University of Glasgow, UK, Paul Anderson University of Edinburgh, James Cheney University of Edinburgh, UK Link to publication Media Attached | ||
17:05 25mTalk | Strong Normalization for Dependent Object Types (DOT) ECOOP Research Papers Link to publication Media Attached |