代数效应与处理器的效应系统
编程语言
2015-07-01 v3 计算机科学中的逻辑
摘要
我们提出了 core Eff 的效应系统，core Eff 是 Eff 的简化变体，而 Eff 是一种具有头等代数效应和处理器的 ML 风格编程语言。我们定义了一个表达力丰富的效应系统，并证明了操作语义相对于该系统的安全性。随后，我们利用 Pitts 的极小不变关系理论，给出了 core Eff 的域论指称语义，并证明了其 adequacy（充分性）。我们利用这一事实开发了寻找有用上下文等价性的工具，包括一个归纳原理。为了展示这些工具的实用性，我们利用它们推导了可变状态的标准方程，包括针对使用非干扰引用的计算的通用交换律。我们已在 Twelf 中形式化了该效应系统、操作语义以及安全性定理。
引用
@article{arxiv.1306.6316,
title = {An Effect System for Algebraic Effects and Handlers},
author = {Andrej Bauer and Matija Pretnar},
journal= {arXiv preprint arXiv:1306.6316},
year = {2015}
}