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.

翻译：会话类型采用线性类型系统，确保通信通道不会被隐式复制或丢弃。因此，这些系统的许多机械化实现需要建模通道上下文，并仔细确保它们以线性方式处理通道。我们展示了一种技术，将线性条件本地化为嵌入类型判断中的附加谓词，从而允许我们使用结构化类型上下文替代线性上下文。在利用（弱）高阶抽象语法处理通道移动性及会话类型系统中出现的复杂绑定结构时，该技术尤为相关。遵循此方法，我们基于经典线性逻辑在证明助理Beluga中机械化了一个会话类型系统及其类型保持证明，其中Beluga使用逻辑框架LF作为其编码语言。我们还证明了编码的充分性。这展示了我们的方法在建模子结构系统（如会话类型语言）中的可操作性和有效性。