IMP在修饰逻辑上有异常

摘要：

在本文中，我们促进不纯的程序设计语言的推理，通过注释术语与“装饰”，描述什么计算（副作用）评估一个术语可能涉及。在一个点自由的范畴语言，称为“装饰逻辑”，我们正式的可变状态和异常的影响，首先分别利用他们之间的anice对偶，然后结合。组合修饰逻辑被用作IMP+Exc命令式程序设计语言的指称语义的目标语言，并允许我们证明用IMP+ Exc编写的程序之间的等价性。

英文摘要：

In this paper, we facilitate the reasoning about impure programming languages, by annotating terms with `decorations' that describe what computational (side) effect evaluation of a term may involve. In a point-free categorical language,called the `decorated logic', we formalize the mutable state and the exception effects first separately, exploiting anice duality between them, and then combined. The combined decorated logic is used as the target language forthe denotational semantics of the IMP+Exc imperative programming language, and allows us to prove equivalencesbetween programs written in IMP+Exc. The combined logic is encoded in Coq, and this encoding is used to certifysome program equivalence proofs.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。