Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library

Kasper Svendsen; Lars Birkedal; Matthew J. Parkinson

Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library

Kasper Svendsen ,
Lars Birkedal ,
Matthew J. Parkinson

ECOOP 2013 - Object-Oriented Programming - 27th European Conference, Montpellier, France, July 1-5, 2013. Proceedings | August 2013

Download BibTex

We present a case study of formal specification for the C $♯ "> ♯$ joins library, an advanced concurrent library implemented using both shared mutable state and higher-order methods. The library is specified and verified in HOCAP, a higher-order separation logic extended with a higher-order variant of concurrent abstract predicates.