LSAM
The Linear Session Abstract Machine (Artefact)
We introduce the Linear SAM, an abstract machine for mechanically executing session-typed programs that precisely correspond to Linear Logic 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 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 CLL proof reductions, and that any CLL proof reduction is simulated by the SAM execution. To that end, we technically factor our development via an intermediate logical language CLLB, which extends 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.
- The Linear Session Abstract Machine March 2026
(Companion to TOPLAS submission) PoC Linear SAM.
Home Page of Luis Caires 