状态和异常效应的Hilbert-Post完备性
Hilbert-Post completeness for the state and the exception effects
摘要：
在本文中，我们提出了一个新的框架来研究计算效果的句法完备性，我们将其应用到例外效果。当应用到国家的影响，我们的框架可以被看作是一个概括的Pretnar的工作在这个问题上。我们首先介绍一个相对概念的希尔伯特-波斯特完整性，非常适合的组合效果。然后，我们证明了异常效果是相对希尔伯特-波斯特完整的，以及“核心”的语言，可用于实现它，这些证明已被形式化，并检查与证明助手Coq。
英文摘要：
In this paper, we present a novel framework for studying the syntactic completeness of computational effects and we apply it to the exception effect. When applied to the states effect, our framework can be seen as a generalization of Pretnar's work on this subject. We first introduce a relative notion of Hilbert-Post completeness, well-suited to the composition of effects. Then we prove that the exception effect is relatively Hilbert-Post complete, as well as the "core" language which may be used for implementing it; these proofs have been formalized and checked with the proof assistant Coq.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
