Implementing a Message-Passing Interpretation of the Semi-Axiomatic Sequent Calculus (Sax)

We present language implementation based on a formulation of sessions types for message-passing programs in terms of an adjoint intuitionistic logic. This logical formulation can naturally describe asynchronous concurrency and can handle linear, affine, multicast and replicated types. This allows the resulting language to express a variety of common programming idioms such as service replicable, broadcast communication and message cancellations within the same programming, while still guaranteeing safety. Our tool consists of a type-checker and an interpreter. It is implemented in the Go language, leveraging its concurrency features in order to investigate the implementability of the operational interpretation proposed by the adjoint logic formulation. We assess the performance of our concurrent interpreter and show that it scales adequately to the number of concurrent processes executed.