Program Logics for Sequential Higher-Order Control
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.
Download: pdf (extended abstract), Status: appeared in FSEN'09.
$Id: index.html,v 1.2 2009/12/04 14:38:39 mfb21 Exp $