Security-typed languages enforce secrecy or integrity policies by type-checking. This paper investigates continuation-passing style as a means of proving that such languages enforce non-interference and as a first step towards understanding their compilation. We present a low-level, secure calculus with higher-order, imperative features. Our type system makes novel use of ordered linear continuations.
(dvi, pdf, ps)