一句话：提出带空间信用与可堆叠断言的高层分离逻辑，在含GC的高层语言中模块化推理堆空间，并在Coq/Iris中机器化验证。
本文研究在带垃圾回收与可变状态的顺序按值调用 lambda 演算中推理堆空间用量的问题。关键难点在于以可靠、模块化且轻量的方式建立内存块的不可达性：已有工作使用 pointed-by 断言追踪每个块的前驱，但局限于类汇编语言。本文将其提升到高层语言，核心挑战是识别并推理垃圾回收器视为根的内存位置。为此，作者提出新颖的“可堆叠”（stackable）断言，在不显式记录来源的情况下追踪栈到堆指针的存在性，并说明如何推理闭包——实现一等函数抽象概念的具体堆分配数据结构。文章通过一系列示例展示该程序逻辑的表达力与可操作性，包括链表上的递归函数、用闭包与可变内部状态实现的对象、续延传递风格（CPS）的递归函数，以及三种具有不同空间界的栈实现；后三者还涉及容器中元素可达性的推理与空间的摊还推理。所有结果均在 Iris 之上用 Coq 机器化证明。
We present a Separation Logic with space credits for reasoning about heap space in a sequential call-by-value lambda-calculus equipped with garbage collection and mutable state. A key challenge is to design sound, modular, lightweight mechanisms for establishing the unreachability of a block. Prior work in this area uses pointed-by assertions to keep track of the predecessors of every block, but is carried out in the setting of an assembly-like programming language. We take up the challenge in the setting of a high-level language, where a key problem is to identify and reason about the memory locations that the garbage collector considers as roots. For this purpose, we propose novel "stackable" assertions, which keep track of the existence of stack-to-heap pointers without explicitly recording their origin. Furthermore, we explain how to reason about closures -- concrete heap-allocated data structures that implement the abstract concept of a first-class function. We demonstrate the expressiveness and tractability of our program logic via a range of examples, including recursive functions on linked lists, objects implemented using closures and mutable internal state, recursive functions in continuation-passing style, and three stack implementations that exhibit different space bounds. These last three examples illustrate reasoning about the reachability of the items stored in a container as well as amortized reasoning about space. All of our results are proved in Coq on top of Iris.
@article{paperbot2106,
title = {A High-Level Separation Logic for Heap Space under Garbage Collection},
author = {Alexandre Moine and Arthur Charguéraud and François Pottier},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571218}
}