We explore the logical underpinnings of higher-order, security-typed
language with mutable state.  Our analysis is based on a logic of
information flow derived from lax logic and the monadic metalanguage.
Thus, our logic deals with mutation explicitly, with impurity
reflected in the types, in contrast to most higher-order
security-typed languages, which deal with mutation implicitly via
side-effects.

More importantly, we also take a store-oriented view of
security, wherein security levels are associated with regions of the
mutable store.  In contrast, most other accounts are
value-oriented, in that security levels are associated with
individual values.  Our store-oriented viewpoint allows us to
address information flow security while still using a largely
conventional logic, but we show that it does not lessen the expressive
power of the logic.  An interesting feature of our analysis lies in
its treatment of upcalls (low-security computations that include
high-security ones), employing an ``informativeness'' judgment
indicating under what circumstances a type carries useful information.