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

Displayed time zone: Osaka, Sapporo, Tokyo change

13:30 - 14:45
Session 6Research Papers at Noh Theater
Chair(s): Johan Jeuring Utrecht University
13:30
25m
Talk
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
25m
Talk
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
25m
Talk
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