By exploiting a number of relatively subtle programming language features, including dynamically-allocated mutable state, first-class functions, and effect handlers, reverse-mode automatic differentiation can be implemented as a library. One outstanding question, however, is: with which logical tools can one specify what this code is expected to compute and verify that it behaves as expected? We answer this question by using a modern variant of Separation Logic to specify and verify a minimalist (but concise and elegant) reverse-mode automatic differentiation library. We view this result as an advanced exercise in program verification, with potential future applications to more realistic automatic differentiation systems.

翻译：通过利用一些相对微妙的编程语言特征,包括动态分布的变异状态、头等功能和效果处理器,可以将反模式自动区分作为图书馆。然而,一个未决问题是:在哪些逻辑工具中可以具体说明该代码预期会如何计算和核实其行为是否如预期?我们用现代的分离逻辑变量来回答这个问题,以具体和核实一个最起码的(但简洁和优雅的)反模式自动区分图库。我们认为这一结果是一种先进的程序核查工作,今后有可能应用到更现实的自动区分系统。