Picture of offices in the City of London

Open Access research that is better understanding work in the global economy...

Strathprints makes available scholarly Open Access content by researchers in the Department of Work, Employment & Organisation based within Strathclyde Business School.

Better understanding the nature of work and labour within the globalised political economy is a focus of the 'Work, Labour & Globalisation Research Group'. This involves researching the effects of new forms of labour, its transnational character and the gendered aspects of contemporary migration. A Scottish perspective is provided by the Scottish Centre for Employment Research (SCER). But the research specialisms of the Department of Work, Employment & Organisation go beyond this to also include front-line service work, leadership, the implications of new technologies at work, regulation of employment relations and workplace innovation.

Explore the Open Access research of the Department of Work, Employment & Organisation. Or explore all of Strathclyde's Open Access research...

Amortised resource analysis with separation logic

Atkey, Robert (2010) Amortised resource analysis with separation logic. In: Proceedings of 19th European Symposium on Programming, ESOP 2010. Lecture Notes in Computer Science, 6012 . Springer, pp. 85-103.

[img]
Preview
PDF
amortised_sep_logic.pdf
Accepted Author Manuscript

Download (262kB) | Preview

Abstract

Type-based amortised resource analysis following Hofmann and Jost—where resources are associated with individual elements of data structures and doled out to the programmer under a linear typing discipline—have been successful in providing concrete resource bounds for functional programs, with good support for inference. In this work we translate the idea of amortised resource analysis to imperative languages by embedding a logic of resources, based on Bunched Implications, within Separation Logic. The Separation Logic component allows us to assert the presence and shape of mutable data structures on the heap, while the resource component allows us to state the resources associated with each member of the structure. We present the logic on a small imperative language with procedures and mutable heap, based on Java bytecode. We have formalised the logic within the Coq proof assistant and extracted a certified verification condition generator. We demonstrate the logic on some examples, including proving termination of in-place list reversal on lists with cyclic tails.