Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity

TL;DR

This paper introduces a novel method to enforce linearity in session types by embedding linearity conditions as predicates within type judgments, enabling the use of structural typing contexts and simplifying mechanization.

Contribution

It presents a technique to localize linearity constraints as predicates, facilitating the mechanization of session-typed systems without requiring linear contexts.

Findings

Successfully mechanized a session-typed system in Beluga

Proved adequacy of the encoding

Demonstrated the approach's effectiveness for substructural systems

Abstract

Session types employ a linear type system that ensures that communication channels cannot be implicitly copied or discarded. As a result, many mechanizations of these systems require modeling channel contexts and carefully ensuring that they treat channels linearly. We demonstrate a technique that localizes linearity conditions as additional predicates embedded within type judgments, which allows us to use structural typing contexts instead of linear ones. This technique is especially relevant when leveraging (weak) higher-order abstract syntax to handle channel mobility and the intricate binding structures that arise in session-typed systems. Following this approach, we mechanize a session-typed system based on classical linear logic and its type preservation proof in the proof assistant Beluga, which uses the logical framework LF as its encoding language. We also prove adequacy for our encoding. This shows the tractability and effectiveness of our approach in modelling substructural systems such as session-typed languages.