一句话：在 Iris 时间信用分离逻辑中机器化重建 Okasaki 的 thunk/debit 摊还推理规则，并验证流与多种队列。
Thunk 是一种可变记忆化数据结构，存储挂起计算或其结果；Okasaki 用 debit 为每个 thunk 标注摊还成本，debit 可分期支付，还可关联尚未分配的未来 thunk，并在未来 thunk 之间转移。本文在 Iris$（带时间信用的丰富分离逻辑）中完整机器化重建了 Okasaki 的 thunk/debit 推理规则，使其可用于形式验证摊还时间复杂度。作者用该规则验证若干 stream 操作，以及 Okasaki 的 physicist's queue、implicit queues 和 banker's queue 等数据结构，表明这些规则足以处理真实摊还分析案例。
A thunk is a mutable data structure that offers a simple memoization service: it stores either a suspended computation or the result of this computation. Okasaki [1999] presents many data structures that exploit thunks to achieve good amortized time complexity. He analyzes their complexity by associating a debit with every thunk. A debit can be paid off in several increments; a thunk whose debit has been fully paid off can be forced. Quite strikingly, a debit is associated also with future thunks, which do not yet exist in memory. Some of the debit of a faraway future thunk can be transferred to a nearer future thunk. We present a complete machine-checked reconstruction of Okasaki’s reasoning rules in Iris $ , a rich separation logic with time credits. We demonstrate the applicability of the rules by verifying a few operations on streams as well as several of Okasaki’s data structures, namely the physicist’s queue, implicit queues, and the banker’s queue.
@article{paperbot2651,
title = {Thunks and Debits in Separation Logic with Time Credits},
author = {François Pottier and Armaël Guéneau and Jacques-Henri Jourdan and Glen Mével},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632892}
}