一句话：提出通用 Dijkstra 单子语义框架，用单子态射为任意单子副作用程序生成验证语义。
论文针对任意单子式副作用的程序验证缺乏通用语义框架的问题，提出 Dijkstra 单子的通用理论。作者将 Dijkstra 单子定义为以规范单子（specification monad）索引的单子状结构，并证明计算单子与规范单子之间的任何单子态射都能诱导出 Dijkstra 单子，从而可按验证任务灵活构造。他们进一步表明，对谓词变换器、Hoare 式前后条件等基规范单子应用单子变换器，可得到大量规范单子；为此提出受 Moggi 单子元语言启发、由依赖类型论参数化的语言来定义正确的单子变换器。论文还发展了 Dijkstra 单子的代数操作概念，并初步探讨两种支持 effect handlers 的方式。该框架在 Coq 和 F* 中实现，支持异常、非确定性、状态、输入输出和一般递归等效应的多种验证风格。
This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effects using Dijkstra monads, which we define as monad-like structures indexed by a specification monad. We prove that any monad morphism between a computational monad and a specification monad gives rise to a Dijkstra monad, which provides great flexibility for obtaining Dijkstra monads tailored to the verification task at hand. We moreover show that a large variety of specification monads can be obtained by applying monad transformers to various base specification monads, including predicate transformers and Hoare-style pre- and postconditions. For defining correct monad transformers, we propose a language inspired by Moggi's monadic metalanguage that is parameterized by a dependent type theory. We also develop a notion of algebraic operations for Dijkstra monads, and start to investigate two ways of also accommodating effect handlers. We implement our framework in both Coq and F*, and illustrate that it supports a wide variety of verification styles for effects such as exceptions, nondeterminism, state, input-output, and general recursion.
@article{paperbot586,
title = {Dijkstra monads for all},
author = {Kenji Maillard and Danel Ahman and Robert Atkey and Guido Martínez and Cătălin Hriţcu and Exequiel Rivas and Éric Tanter},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341708}
}