一句话：把线性条件嵌入类型判断，用结构上下文在 Beluga 中机械化会话类型及类型保持证明。
会话类型依赖线性类型系统来保证通信通道不被隐式复制或丢弃，因此其机械化通常需要线性上下文并小心处理通道。本文提出一种结构化视角：将线性条件局部化为嵌入类型判断的额外谓词，从而可用结构类型的上下文代替线性上下文；该方法特别适合结合弱高阶抽象语法（weak HOAS）处理通道移动性及复杂绑定结构。作者在证明助手 Beluga 中（编码语言为 LF）机械化了一个基于经典线性逻辑的会话类型系统及其类型保持证明，并证明了编码的 adequacy。结果展示了该方法在建模会话类型等子结构系统时的可操作性与有效性。
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.
@article{paperbot1824,
title = {Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity},
author = {Chuta Sano and Ryan Kavanagh and Brigitte Pientka},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622810}
}