A High-Level Separation Logic for Heap Space under Garbage Collection (Extended Version)

We present a Separation Logic with space credits for reasoning about heapspace in a sequential call-by-value lambda-calculus equipped with garbagecollection and mutable state. A key challenge is to designsound, modular, lightweight mechanisms for establishing the unreachability ofa block. Prior work in this area uses pointed-by assertions to keep track ofthe predecessors of every block, but is carried out in the setting of anassembly-like programming language. We take up the challenge in the setting ofa high-level language, where a key problem is to identify and reason about thememory locations that the garbage collector considers as roots. For thispurpose, we propose novel "stackable" assertions, which keep track of theexistence of stack-to-heap pointers without explicitly recording their origin.Furthermore, we explain how to reason about closures -- concreteheap-allocated data structures that implement the abstract concept of afirst-class function. We demonstrate the expressiveness and tractability ofour program logic via a range of examples, including recursive functions onlinked lists, objects implemented using closures and mutable internal state,recursive functions in continuation-passing style, and three stackimplementations that exhibit different space bounds. These last three examplesillustrate reasoning about the reachability of the items stored in a containeras well as amortized reasoning about space. All of our results are proved inCoq on top of Iris