2016/11/18 by Simon Fowler, Sam Lindley, Fowler, Simon +3
Computer Science · #Logic, programming, and type systems #Computability, Logic, AI Algorithms #Cellular Automata and Applications
paper · doi:10.48550/arxiv.1611.06276
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 λ_\textrmch for typed asynchronous channels, and a calculus λ_\textrmact for typed actors. We define translations from λ_\textrmact into λ_\textrmch and λ_\textrmch into λ_\textrmact 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.