M. Abadi and C. Fournet, Access control based on execution history, Proceedings of NDSS'03, pp.107-121, 2003.

J. Agat, Transforming out timing leaks, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, pp.40-53, 2000.
DOI : 10.1145/325694.325702
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.9484

K. R. Apt and E. Olderog, Verification of sequential and concurrent programs, 1991.

B. E. Aydemir, A. Bohannon, M. Fairbairn, J. N. Foster, B. C. Pierce et al., Mechanized Metatheory for the Masses: The PoplMark Challenge, Proceedings of TPHOLs'05, pp.50-65, 2005.
DOI : 10.1007/11541868_4

C. Ballarin, Locales and Locale Expressions in Isabelle/Isar, Proceedings of TYPES'03, pp.34-50, 2003.
DOI : 10.1007/978-3-540-24849-1_3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.801

A. Banerjee and D. Naumann, Stack-based access control and secure information flow, Journal of Functional Programming, vol.15, issue.2, pp.131-177, 2005.
DOI : 10.1017/S0956796804005453

A. Banerjee and D. A. Naumann, Secure Information Flow and Pointer Confinement in a Java-like Language, Proceedings of CSFW'02, 2002.

G. Barthe, P. D. Argenio, and T. Rezk, Secure Information Flow by Self- Composition, Proceedings of CSFW'04, pp.100-114, 2004.
DOI : 10.1109/csfw.2004.1310735
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.378.849

G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, S. Melo et al., A Formal Executable Semantics of the JavaCard Platform, Proceedings of ESOP'01, pp.302-319, 2001.
DOI : 10.1007/3-540-45309-1_20

G. Barthe and L. Prensa-nieto, Formally verifying information flow type systems for concurrent and thread systems, Proceedings of the 2004 ACM workshop on Formal methods in security engineering , FMSE '04, pp.13-22, 2004.
DOI : 10.1145/1029133.1029136
URL : https://hal.archives-ouvertes.fr/inria-00000632

G. Boudol, ULM: A Core Programming Model for Global Computing, Proceedings of ESOP'04, pp.234-248, 2004.
DOI : 10.1007/978-3-540-24725-8_17

G. Boudol and I. Castellani, Noninterference for Concurrent Programs, Proceedings of ICALP'01, pp.382-395, 2001.
DOI : 10.1007/3-540-48224-5_32
URL : https://hal.archives-ouvertes.fr/inria-00072334

G. Boudol and I. Castellani, Noninterference for concurrent programs and thread systems, Theoretical Computer Science, vol.281, issue.1-2, pp.109-130, 2002.
DOI : 10.1016/S0304-3975(02)00010-5
URL : https://hal.archives-ouvertes.fr/inria-00072334

M. Dam, Decidability and proof systems for language-based noninterference relations, Proceedings of POPL'06, pp.67-78, 2006.

Z. Deng and G. Smith, Lenient array operations for practical secure information flow, Proceedings of CSFW'04, pp.115-124, 2004.

R. Focardi and R. Gorrieri, Classification of Security Properties, Foundations of Security Analysis and Design, pp.331-396, 2001.
DOI : 10.1007/3-540-45608-2_6

R. Focardi, S. Rossi, and A. Sabelfeld, Bridging Language-Based and Process Calculi Security, Proceedings of FOS- SACS'05, pp.299-315, 2005.
DOI : 10.1007/978-3-540-31982-5_19

J. Goguen and J. Meseguer, Security Policies and Security Models, 1982 IEEE Symposium on Security and Privacy, pp.11-22, 1982.
DOI : 10.1109/SP.1982.10014

M. Hennessy and J. Riely, Information flow vs. resource access in the asynchronous pi-calculus, Proceedings of ICALP'00, pp.415-427, 2000.
DOI : 10.1145/570886.570890

T. A. Henzinger, C. M. Kirsch, and S. Matic, Schedule-Carrying Code, Proceedings of EMSOFT'03, pp.241-256, 2003.
DOI : 10.1007/978-3-540-45212-6_16

K. Honda, V. Vasconcelos, and N. Yoshida, Secure Information Flow as Typed Process Behaviour, Proceedings of ESOP'00, pp.180-199
DOI : 10.1007/3-540-46425-5_12

K. Honda and N. Yoshida, A Uniform Type Structure for Secure Information Flow, Proceedings of POPL'02, pp.81-92, 2002.

M. Huisman, P. Worah, and K. Sunesen, A temporal logic characterisation of observational determinism, Proceedings of CSFW'06, pp.3-15, 2006.

R. Joshi and K. R. Leino, A semantic approach to secure information flow, Science of Computer Programming, vol.37, issue.1-3, pp.1-3113, 2000.
DOI : 10.1016/S0167-6423(99)00024-6

K. Leino and R. Joshi, A semantic approach to secure information flow, Proceedings of MPC'98, pp.254-271, 1998.

H. Mantel and A. Sabelfeld, A unifying approach to the security of distributed and multi-threaded programs1, Journal of Computer Security, vol.11, issue.4, pp.615-676, 2003.
DOI : 10.3233/JCS-2003-11406

H. Mantel, H. Sudbrock, and T. Krausser, Combining Different Proof Techniques for Verifying Information Flow Security, Pre- Proceedings of LOPSTR'06, volume Raporta di Ricerca CS-2006-5, 2006.
DOI : 10.1007/978-3-540-71410-1_8

A. , A. Matos, and G. Boudol, On declassification and the nondisclosure policy, Proceedings of CSFW'05, pp.226-240, 2005.

A. Almeida-matos, G. Boudol, and I. Castellani, Typing noninterference for reactive programs, Proceedings of FCS'04, 2004.
DOI : 10.1016/j.jlap.2007.02.009
URL : https://hal.archives-ouvertes.fr/inria-00070413

M. Montgomery and K. Krishna, Secure Object Sharing in Java Card, Proceedings of Usenix workshop on Smart Card Technology, 1999.

D. Naumann, Machine-checked correctness of a secure information flow analyzer (preliminary report), 2003.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science, 2002.
DOI : 10.1007/3-540-45949-9

L. C. Paulson, The Isabelle Reference Manual

F. Pottier, A simple view of type-secure information flow in the pi-calculus, Proceedings of CSFW'02, pp.320-330, 2002.

C. Röckl and D. Hirschkoff, A fully adequate shallow embedding of the ??-calculus in Isabelle/HOL with mechanized syntax analysis, Journal of Functional Programming, vol.13, issue.02, pp.415-451, 2003.
DOI : 10.1017/S0956796802004653

J. Rushby, Noninterference, transitivity, and channel-control security policies, 1992.

A. Russo and A. Sabelfeld, Securing Interaction between Threads and the Scheduler, 19th IEEE Computer Security Foundations Workshop (CSFW'06), 2006.
DOI : 10.1109/CSFW.2006.29

A. Sabelfeld, The Impact of Synchronisation on Secure Information Flow in Concurrent Programs, Proceedings of PSI'01, pp.227-241, 2001.
DOI : 10.1007/3-540-45575-2_22

A. Sabelfeld and A. Myers, Language-based information-flow security, IEEE Journal on Selected Areas in Communications, vol.21, issue.1, pp.5-19, 2003.
DOI : 10.1109/JSAC.2002.806121
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.3979

A. Sabelfeld and A. Myers, A Model for Delimited Information Release, Proceedings of ISSS'03, pp.174-191, 2004.
DOI : 10.1007/978-3-540-37621-7_9

A. Sabelfeld and D. Sands, A Per Model of Secure Information Flow in Sequential Programs, Proceedings of ESOP'99, pp.40-58, 1999.
DOI : 10.1007/3-540-49099-X_4

A. Sabelfeld and D. Sands, A per model of secure information flow in sequential programs. Higher-Order and Symbolic Computation, pp.59-91, 2001.

A. Sabelfeld and D. Sands, Dimensions and principles of declassification, Proceedings of CSFW'05, 2005.

D. Sangiorgi and D. Walker, The ?-calculus: a Theory of Mobile Processes, 2001.

G. Smith, A new type system for secure information flow, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., pp.115-125, 2001.
DOI : 10.1109/CSFW.2001.930141

G. Smith and D. 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
URL : http://cisr.nps.edu/downloads/98paper_multithread.pdf

M. Strecker, Formal analysis of an information flow type system for MicroJava (extended version), 2003.

D. Volpano and G. Smith, A type-based approach to program security, Proceedings of TAPSOFT'97, pp.607-621, 1997.
DOI : 10.1007/BFb0030629

D. Volpano and G. Smith, Probabilistic noninterference in a concurrent language, Proceedings. 11th IEEE Computer Security Foundations Workshop (Cat. No.98TB100238), pp.34-43, 1998.
DOI : 10.1109/CSFW.1998.683153

D. Volpano and G. Smith, Probabilistic noninterference in a concurrent language, Proceedings. 11th IEEE Computer Security Foundations Workshop (Cat. No.98TB100238), pp.231-253, 1999.
DOI : 10.1109/CSFW.1998.683153

D. M. Volpano and G. Smith, Verifying secrets and relative secrecy, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, pp.268-276, 2000.
DOI : 10.1145/325694.325729
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.152.7333

S. Zdancewic and A. C. Myers, Observational determinism for concurrent program security, 16th IEEE Computer Security Foundations Workshop, 2003. Proceedings., pp.29-46, 2003.
DOI : 10.1109/CSFW.2003.1212703
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.3238