Higher-Order Linearisability
View/ Open
Publisher
Journal
Journal of Logical and Algebraic Methods in Programming
ISSN
2352-2208
Metadata
Show full item recordAbstract
Linearisability is a central notion for verifying concurrent libraries: a library is proven
correct if its operational history can be rearranged into a sequential one that satisfies a
given specification. Until now, linearisability has been examined for libraries in which
method arguments and method results were of ground type. In this paper we extend
linearisability to the general higher-order setting, where methods of arbitrary type can
be passed as arguments and returned as values, and establish its soundness.