Continuations in possible-world semantics

AbstractEarlier work has shown that a form of possible-world semantics allows elegant solutions to certain difficult problems in the modelling of local-variable declarations and noninterference specifications in a generalization of Hoare's logic suitable for algol 60-like languages with procedures. In this work it is shown how jumps and block expressions can be treated in this framework