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

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

. ). Needs, 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

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

A. Joseph, J. Goguen, and . Meseguer, Security policies and security models, Proc. IEEE Symp. Security and Privacy, pp.11-20, 1982.

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

G. Kahn, 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

A. Gurvan-le-guernic, T. Banerjee, D. Jensen, and . Schmidt, Automatonbased confidentiality monitoring, Proceedings of the 11th Annual Asian Computing Science Conference, 2006.

F. Nielson, H. R. Nielson, and C. Hankin, Principles of Program Analysis, 1999.
DOI : 10.1007/978-3-662-03811-6

W. O. Peter and . Hearn, Resources, Concurrency and Local Reasoning, Gardner and Yoshida, pp.49-67

A. Russo, J. Hughes, D. Naumann, and A. Sabelfeld, Closing Internal Timing Channels by Transformation, Proceedings of the 11th Annual Asian Computing Science Conference, 2006.
DOI : 10.3233/JCS-1996-42-304

]. A. Sab01 and . Sabelfeld, 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.

D. [. Smith and . Volpano, 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