Type systems equivalent to data-flow analyses for imperative languages

We show that a large class of data-flow analyses for imperative languages are describable as type systems in the following technical sense: possible results of an analysis can be described in a language of types so that a program checks with a type if and only if this type is a supertype of the result of applying the analysis. Type-checking is easy with the help of a certificate that records the “eureka”-bits of a typing derivation. Certificate-assisted type-checking amounts to a form of lightweight analysis à la Rose. For secure information flow, we obtain a type system that is considerably more precise than that of Volpano et al., but not more sophisticated. Importantly, our type systems are compositional.