Proving Noninterference by Fully Complete Translation to the Symply Typed λ-Calculus

By Naokata Shikuma and Atsushi Igarashi. Logical Methods in Computer Science, 4(3:10), pages. 1-31, September 2008.

A preliminary version appeared in Proceedings of the 11th Annual Asian Computing Science Conference (ASIAN'06), pages 302-316, Springer LNCS 4435, Tokyo, Japan, December 2006.


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 λ→, using fully complete translation to λ→. Full completeness plays an important role in showing preservation of the two logical relations through the translation.

PDF file(s)