paper on language translations and security

The following paper on languages and security is available from URL

            Protection in Programming-Language Translations

    We discuss abstractions for protection and the correctness of 
    their implementations. Relying on the concept of full abstraction, 
    we consider two examples: (1) the translation of Java classes 
    to an intermediate bytecode language, and (2) in the setting 
    of the pi calculus, the implementation of private channels in 
    terms of cryptographic operations.             

Although the paper is not primarily about types, parts of it might 
interest some readers of this list. 

Martin Abadi