Wed 18 Jan 2023 13:30 - 13:55 at Avenue34 - Program Logics & Resources Chair(s): Robbert Krebbers

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.

Wed 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 14:45
Program Logics & ResourcesPOPL at Avenue34
Chair(s): Robbert Krebbers Radboud University Nijmegen
A High-Level Separation Logic for Heap Space under Garbage Collection
Alexandre Moine Inria, Arthur Charguéraud Inria; Université de Strasbourg; CNRS; ICube, François Pottier Inria
CN: Verifying Systems C Code with Separation-Logic Refinement Types
Christopher Pulte University of Cambridge, Dhruv C. Makwana University of Cambridge, Thomas Sewell University of Cambridge, Kayvan Memarian University of Cambridge, Peter Sewell University of Cambridge, Neel Krishnaswami University of Cambridge
Conditional Contextual Refinement
Youngju Song Seoul National University; MPI-SWS, Minki Cho Seoul National University, Dongjae Lee Seoul National University, Chung-Kil Hur Seoul National University, Michael Sammler MPI-SWS, Derek Dreyer MPI-SWS