Program logics for sequential higher-order control

Berger, Martin (2010) Program logics for sequential higher-order control. In: Arbab, F and Sirjani, M (eds.) Fundamentals of software engineering: Third IPM International Conference, FSEN 2009, Kish Island, Iran, April 15-17, 2009, Revised Selected Papers. Lecture Notes in Computer Science, 5961 . Springer Verlag, Berlin, pp. 194-211. ISBN 978-3-642-11622-3

[img] PDF
Restricted to SRO admin only

Download (182kB)


We introduce a Hoare logic for call-by-value higher-order functional languages with control operators such as callcc. The key idea is to build the assertion language and proof rules around an explicit logical representation of jumps and their dual 'places-to-jump-to'. This enables the assertion language to capture precisely the intensional and extensional effects of jumping by internalising rely/guarantee reasoning, leading to simple proof rules for higher-order functions with callcc. We show that the logic can reason easily about non-trivial uses of callcc. The logic matches exactly with the operational semantics of the target language (observational completeness), is relatively complete in Cook's sense and allows efficient generation of characteristic formulae.

Item Type: Book Section
Schools and Departments: School of Engineering and Informatics > Informatics
Related URLs:
Depositing User: Martin Berger
Date Deposited: 06 Feb 2012 19:54
Last Modified: 13 Nov 2013 14:55

View download statistics for this item

📧 Request an update