Program Logics for Sequential Higher-Order Control

14 years 4 days ago
Program Logics for Sequential Higher-Order Control
We introduce a Hoare logic for 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 nd/or λµ-like name-abstraction. We show that the logic can reason easily about non-trivial examples of using 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. Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs—Assertions, Specification Techniques Keywords Program Logics, T...
Martin Berger
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where FSEN
Authors Martin Berger
Comments (0)