jung_higher-order_2016:
  type: article
  title: Higher-order ghost state
  author:
  - Jung, Ralf
  - Krebbers, Robbert
  - Birkedal, Lars
  - Dreyer, Derek
  date: 2016-09
  page-range: 256-269
  url:
    value: https://dl.acm.org/doi/10.1145/2951913.2951943
    date: 2024-11-14
  serial-number:
    doi: 10.1145/2951913.2951943
    isbn: 978-1-4503-4219-3
  abstract: '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.'
  parent:
    type: proceedings
    title: Proceedings of the 21st {ACM} {SIGPLAN} {International} {Conference} on {Functional} {Programming}
    publisher:
      name: Association for Computing Machinery
      location: New York, NY, USA
    parent:
      type: proceedings
      title: '{ICFP} 2016'