Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Tue 20 Sep 2016 14:20 - 14:45 at Noh Theater - Session 6 Chair(s): Johan Jeuring

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 Sep

13:30 - 14:45: Research Papers - Session 6 at Noh Theater
Chair(s): Johan JeuringUtrecht University
icfp-2016-papers13:30 - 13:55
Eric SeidelUniversity of California at San Diego, USA, Ranjit JhalaUniversity of California at San Diego, USA, Westley WeimerUniversity of Virginia, USA
icfp-2016-papers13:55 - 14:20
Keiichi WatanabeUniversity of Tokyo, Japan, Ryosuke SatoUniversity of Tokyo, Japan, Takeshi TsukadaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan
icfp-2016-papers14:20 - 14:45
Ralf JungMPI-SWS, Germany, Robbert KrebbersAarhus University, Denmark, Lars BirkedalAarhus University, Denmark, Derek DreyerMPI-SWS, Germany