Proving Noninterference by a Fully Complete Translation to the Simply Typed Lambda-Calculus. - Naokata Shikuma; Atsushi Igarashi (Log. Methods Comput. Sci., 2008)