Computer Science – Programming Languages
Scientific paper
2008-08-25
LMCS 4 (3:10) 2008
Computer Science
Programming Languages
31 pages
Scientific paper
10.2168/LMCS-4(3:10)2008
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 preserves the logical relations defined for both calculi. In fact, we have found a counterexample for it. In this article, instead of DCC, we prove noninterference for sealing calculus, a new variant of DCC, by reduction to the basic lemma of a logical relation for the simply typed lambda-calculus, using a fully complete translation to the simply typed lambda-calculus. Full completeness plays an important role in showing preservation of the two logical relations through the translation. Also, we investigate relationship among sealing calculus, DCC, and an extension of DCC by Tse and Zdancewic and show that the first and the last of the three are equivalent.
Igarashi Atsushi
Shikuma Naokata
No associations
LandOfFree
Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-380347