ML5 的单子形式化

ML5 是一种用于空间分布式计算的编程语言，基于与模态逻辑 S5 的 Curry-Howard 对应。尽管 ML5 是通过与 S5 模态逻辑的对应来设计的，但该编程语言在若干方面与逻辑有所不同。在本文中，我们通过将 ML5 翻译为一种略有不同的逻辑来解释这些差异：即扩展了松弛模态的直觉主义 S5，该松弛模态将有效计算封装在单子中。这种翻译既解释了现有的 ML5 设计，又提出了一些简化与泛化。我们在 Agda 证明助手中形式化了我们的翻译。我们没有将松弛 S5 形式化为一种证明论，而是将其作为宇宙嵌入到依值类型宿主语言中，该宇宙消去通过实现模态逻辑的 Kripke 语义来给出。这种表示技术省去了为逻辑定义证明论并证明其正确性的工作，此外还允许我们继承元语言的等式理论，这可用于证明语义验证了 ML5 的操作语义。