Search

• < Previous
• 1
• Next >

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

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 parametricity of System F. Unfortunately, their proof contains errors in a key lemma that their translation from DCC to System F&nbsp;[&hellip;]