Zdancewic, S., Myers, A.C. Secure Information Flow via Linear Continuations. Higher-Order and Symbolic Computation 15, 209–234 (2002).

Remarkable PDF

Original PDF



Security-typed languages enforce secrecy or integrity policies by type-checking. This paper investigates continuation-passing style (CPS) as a means of proving that such languages enforce noninterference and as a first step towards understanding their compilation. We present a low-level, secure calculus with higher-order, imperative features and linear continuations.

Linear continuations impose a stack discipline on the control flow of programs. This additional structure in the type system lets us establish a strong information-flow security property called noninterference. We prove that our CPS target language enjoys the noninterference property and we show how to translate secure high-level programs to this low-level language. This noninterference proof is the first of its kind for a language with higher-order functions and state.


  • Extended version of [Zdancewic2001]
  • Calls out that ordered linear continuations yield a stack discipline for control flow.