Monad-independent Dynamic Logic in HasCasl
Monad-independent Dynamic Logic in HasCasl
复制标题
HasCasl 中独立于 Monad 的动态逻辑
DOI：
10.1093/logcom/14.4.571
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Till Mossakowski
中科院分区：
文献类型：
--
作者：
Lutz Schröder;Till Mossakowski
Monads被Moggi认为是处理函数式编程语言中有状态计算的一种优雅的方法。在之前的工作中，我们引入了一元程序部分正确性的Hoare演算。所有这些都是以一种完全独立于单子的方式完成的。在这里，我们将其扩展到与monad无关的动态逻辑（假设monad有适量的额外基础设施）。动态逻辑比霍尔演算更有表现力;特别是，它允许关于终止和完全正确性的推理。作为这些概念的背景形式主义，我们使用HASCASL的逻辑，高阶语言的功能规范和编程。
Monads have been recognized by Moggi as an elegant device for dealing with stateful computation in functional programming languages. In previous work, we have introduced a Hoare calculus for partial correctness of monadic programs. All this has been done in an entirely monad-independent way. Here, we extend this to a monad-independent dynamic logic (assuming a moderate amount of additional infrastructure for the monad). Dynamic logic is more expressive than the Hoare calculus; in particular, it allows reasoning about termination and total correctness. As the background formalism for these concepts, we use the logic of HASCASL, a higher-order language for functional specification and programming.