Playing with Bisimulation in Erlang

Ivan Lanese (1, 2) , Davide Sangiorgi (1, 2) , Gianluigi Zavattaro (1, 2)

1 FOCUS - Foundations of Component-based Ubiquitous Systems
2 UNIBO - Alma Mater Studiorum Università di Bologna = University of Bologna

Erlang is a functional and concurrent programming language. The aim of this paper is to investigate basic properties of the Erlang concurrency model, which is based on asynchronous communication through mailboxes accessed via pattern matching. To achieve this goal, we consider Core Erlang (which is an intermediate step in Erlang compilation) and we define, on top of its operational semantics, an observational semantics following the approach used to define asynchronous bisimulation for the π-calculus. Our work allows us to shed some light on the management of process identifiers in Erlang, different from the various forms of name mobility already studied in the literature. In fact, we need to modify standard definitions to cope with such specific features of Erlang.

Domaines: Langage de programmation [cs.PL]; Théorie et langage formel [cs.FL]

Ivan Lanese, Davide Sangiorgi, Gianluigi Zavattaro. Playing with Bisimulation in Erlang. Models, Languages, and Tools for Concurrent and Distributed Programming, 2019, ⟨10.1007/978-3-030-21485-2_6⟩. ⟨hal-02376217⟩