Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library - Svendsen, Kasper; Birkedal, Lars; Parkinson, Matthew J. (ECOOP 2013 - Object-Oriented Programming - 27th European Conference, Montpellier, France, July 1-5, 2013. Proceedings, 2013)
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.