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.
$Date: 2008-09-22 15:19:01 +0900 (Mon, 22 Sep 2008) $