Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus

Naokata Shikuma, Atsushi Igarashi

Tse and Zdancewic have formalized the notion of noninterference for Abadi et al.'s DCC in terms of logical relations and given a proof of noninterference by reduction to parametric…