The development of concurrent separation logic (CSL) has sparked a long line of work on modular verification of sophisticated concurrent programs. Two of the most important features supported by several existing extensions to CSL are higher-order quantification and custom ghost state. However, none of the logics that support both of these features reap the full potential of their combination. In particular, none of them provide general support for a feature we dub "higher-order ghost state": the ability to store arbitrary higher-order separation-logic predicates in ghost variables.
In this paper, we propose higher-order ghost state as a interesting and useful extension to CSL, which we formalize in the framework of Jung et al.'s recently developed Iris logic. To justify its soundness, we develop a novel algebraic structure called CMRAs ("cameras"), which can be thought of as "step-indexed partial commutative monoids". Finally, we show that Iris proofs utilizing higher-order ghost state can be effectively formalized in Coq, and discuss the challenges we faced in formalizing them.
Tue 20 SepDisplayed time zone: Osaka, Sapporo, Tokyo change
13:30 - 14:45 | |||
13:30 25mTalk | Dynamic Witnesses for Static Type Errors (or, Ill-Typed Programs Usually Go Wrong) Research Papers Eric Seidel University of California at San Diego, USA, Ranjit Jhala University of California at San Diego, USA, Westley Weimer University of Virginia, USA DOI | ||
13:55 25mTalk | Automatically Disproving Fair Termination of Higher-Order Functional Programs Research Papers Keiichi Watanabe University of Tokyo, Japan, Ryosuke Sato University of Tokyo, Japan, Takeshi Tsukada University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan DOI | ||
14:20 25mTalk | Higher-Order Ghost State Research Papers Ralf Jung MPI-SWS, Germany, Robbert Krebbers Aarhus University, Denmark, Lars Birkedal Aarhus University, Denmark, Derek Dreyer MPI-SWS, Germany DOI | ||