Proving Noninterference by a Fully Complete Translation to the Simply Typed λ-Calculus
Naokata Shikuma, Atsushi Igarashi · Lecture notes in computer science · 2007
Tse and Zdancewic have formalized the notion of noninterference for Abadi et al.’s DCC in terms of logical relations and given a proof by reduction to parametricity of System F. Unfortunately, their proof contains errors in a key lemma that their translation from DCC to System F preserves the logical relations defined for both calculi. We prove noninterference for a variant of DCC by reduction to the basic lemma of a logical relation for the simply typed λ -calculus, using a fully complete translation to the simply typed λ -calculus. Full completeness plays an important role in showing preservation of the two logical relations through the translation.