Security Type Systems as Recursive Predicates

Andrei Popescu

We show how security type systems from the literature of language-based noninterference can be represented more directly as predicates defined by structural recursion on the progra…