域感知会话类型（扩展版）

我们基于带有混合逻辑特征（特别是表示域的模态世界）的线性逻辑扩展，发展了现有（二元）会话类型的柯里-霍华德解释的推广。这些世界管控域迁移，并服从模态逻辑克里普克语义中熟悉的参数化可达关系。其结果是一个用于域感知、消息传递并发的富有表现力的新型类型化进程框架。其逻辑基础确保了良类型进程享有会话保真度、全局进展和终止性。类型化还确保进程仅与可达域通信，从而遵守可达关系。值得注意的是，我们的域感知框架可以指定域信息仅在运行时可用的场景；灵活的可达关系可以被干净地定义并静态强制。作为一个具体应用，我们引入了域感知多方会话类型，其中全局协议可通过域迁移表达任意嵌套的子协议。我们通过归约到我们的二元域感知框架，对这些多方协议进行了精确分析：复杂的域感知协议可以在恰当的抽象层次上被推理，也确保了关键正确性属性从二元到多方设置的原则性迁移。