A monadic analysis of information flow security with mutable state. - Karl Crary; Aleksey Kliger; Frank Pfenning (J. Funct. Program., 2005)