Encoding Asynchrony in Choreographies

Choreographies are widely used both for the specification and the programming of concurrent and distributed software architectures. Since many of such architectures use asynchronous communications, it is essential to understand how the behaviour described in a choreography can be correctly implemented in asynchronous settings. So far, this problem has been addressed by relying on additional technical machinery, such as ad-hoc syntactic terms, semantics, or equivalences. In this work, we show that such extensions are not needed for choreography languages that support primitives for process spawning and name mobility. Instead, we can just encode asynchronous communications in choreographies themselves, yielding a simpler approach.