The Linear Session Abstract Machine

We introduce the Linear SAM, an abstract machine for mechanically executing session-typed programs that precisely correspond to Linear Logic \(\mathsf{CLL}\) via the propositions-as-types correspondence. In this basic computation model, programs are naturally interpreted as concurrent systems. However, inspired by a fine-grained analysis of proof conversion and focalisation, we derive in this work a fully deterministic sequential evaluation strategy, which may be implemented via co-routining and session buffered communication. Our development targets a language extending \(\mathsf{CLL}\) with second-order quantifiers (polymorphism) and inductive types (recursion and co-recursion), which supports general higher-order polymorphic functional / session-based computation. A remarkable feature of the SAM’s design is its ability to seamlessly coordinate sequential session behaviour with concurrent session behaviour within the same program. We provide an intuitive discussion of the SAM structure and its underlying design, and state and prove its adequacy, showing that SAM executions always correspond to \(\mathsf{CLL}\) proof reductions, and that any \(\mathsf{CLL}\) proof reduction is simulated by the SAM execution. To that end, we technically factor our development via an intermediate logical language \(\mathsf{CLLB}\) , which extends \(\mathsf{CLL}\) with a “buffered” cut construct, and bridges between the logical/algebraic level and the lower-level machine architecture. We also discuss a proof-of-concept implementation of the SAM, that suggests its potential to support the native linear execution of general session-functional linear programming languages with concurrency.