The proof goes by induction on the derivation tree of the global hypothesis ? 5 . If the last typing rule used is ,

The global hypothesis ? 4 and the local conclusion (1) imply w ? {?} ? . The global hypothesis ? ?? and the local conclusion (1) imply FV(e) ,

S true ) ? needs(S false ) = ?. If FV(e) ? V ? then there exists a variable z in FV(e) such that z ? V. The global hypothesis ? 2 implies that ?(z) = H. Then ?(e) = H. Therefore, lemma A.9 and the local conclusion (1) imply needs(S true ) = needs(S false ) = ? (3) FV(e) ? V ? implies that both S true and S f alse can be typed as H cmd with the typing environment ?. If FV(e) ? V ? then there exists a variable z in FV(e) such that z ? V, The global hypothesis ? 2 implies that ?(z) = H. Then ?(e) = H and the desired result follows from the local conclusion ,

A semantics for concurrent separation logic, Gardner and Yoshida, pp.16-34 ,

Security policies and security models, Proc. IEEE Symp. Security and Privacy, pp.11-20, 1982. ,

Towards a theory of parallel programming, Operating Systems Techniques, pp.61-71, 1972. ,

Natural semantics, Proceedings of the Symposium on Theoretical Aspects of Computer Science, pp.22-39, 1987. ,

DOI : 10.1007/BFb0039592

URL : https://hal.archives-ouvertes.fr/inria-00075953

Automatonbased confidentiality monitoring, Proceedings of the 11th Annual Asian Computing Science Conference, 2006. ,

Principles of Program Analysis, 1999. ,

DOI : 10.1007/978-3-662-03811-6

Resources, Concurrency and Local Reasoning, Gardner and Yoshida, pp.49-67 ,

Closing Internal Timing Channels by Transformation, Proceedings of the 11th Annual Asian Computing Science Conference, 2006. ,

DOI : 10.3233/JCS-1996-42-304

The impact of synchronisation on secure information flow in concurrent programs, Proc. Andrei Ershov International Conference on Perspectives of System Informatics, pp.227-241, 2001. ,

Secure information flow in a multi-threaded imperative language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.355-364, 1998. ,

DOI : 10.1145/268946.268975