A Continuation-Based Solution of the Linearity Challenge

The formalisation of session calculi is made difficult by the management of session channels, which are linear resources that cannot be discarded or duplicated and whose type changes over time, as input/output operations are performed on them. Context splitting, the channel management technique directly related to the way session type theories are usually written with pen and paper, is often considered a hindrance and a notable source of complexity, to the point where several alternative approaches have been recently proposed. In this paper we describe the Agda formalisation of a process calculus based on classical linear logic that supports the modeling of binary sessions through their encoding with explicit continuation channels. The formalisation turns out to be remarkably compact despite the adoption of context splitting. We argue that the logical nature of the calculus and the use of explicit continuations are contributing factors to the simplicity of its formalisation.