Proving noninterference by a fully complete translation to the simply typed λ-calculus

摘要: Tse and Zdancewic have formalized the notion of noninterference for Abadi et al.'s DCC in terms logical relations given a proof by reduction to parametricity System F. Unfortunately, their contains errors key lemma that translation from F preserves defined both calculi. We prove variant basic relation simply typed λ-calculus, using fully complete λ-calculus. Full completeness plays an important role showing preservation two through translation.