A. Banerjee and D. Naumann, Stack-based access control and secure information flow, Journal of Functional Programming, vol.15, issue.2, 2003.
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, A. Basu, and T. Rezk, Security types preserving compilation, Proceedings of VMCAI'04, pp.2-15
DOI : 10.1016/j.cl.2005.05.002
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.598.8956

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

S. Crafa, M. Bugliesi, and G. Castagna, Information flow security for boxed ambients) of Electronic Notes in Theoretical Computer Science, Proceedings of F-WAN, 2002.

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

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, J. Riely, and V. ). U=p, Information flow vs. resource access in the asynchronous pi-calculus, Proceedings of ICALP'00, volume 1853 of Lecture Notes in Computer Science, 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 and N. Yoshida, A Uniform Type Structure for Secure Information Flow, Proceedings of POPL'02, pp.81-92, 2002.

G. Klein and T. Nipkow, Verified bytecode verifiers, Theoretical Computer Science, vol.298, issue.3, pp.583-626, 2002.
DOI : 10.1016/S0304-3975(02)00869-1

G. Klein and M. Strecker, Verified bytecode verification and type-certifying compilation, The Journal of Logic and Algebraic Programming, vol.58, issue.1-2, pp.27-60, 2004.
DOI : 10.1016/j.jlap.2003.07.004
URL : http://doi.org/10.1016/j.jlap.2003.07.004

H. Mantel and D. Sands, Controlled Declassification Based on Intransitive Noninterference, Proceedings of APLAS'04, 2004.
DOI : 10.1007/978-3-540-30477-7_9

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

A. C. Myers, A. Sabelfeld, and S. Zdancewic, Enforcing robust declassification, Proceedings. 17th IEEE Computer Security Foundations Workshop, 2004., pp.172-186, 2004.
DOI : 10.1109/CSFW.2004.1310740
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.147.2865

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

/. Isabelle and . Hol, A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science, 2002.

D. Oheimb, Analyzing Java in Isabelle/HOL: Formalization, Type Safety and Hoare Logic, 2001.

F. Pottier and V. Simonet, Information flow inference for ML, Proceedings of POPL'02, pp.319-330

C. Röckl and D. Hirschkoff, A fully adequate shallow embedding of the ?-calculus in Isabelle/HOL with mechanized syntax analysis, and channel-control security policies, Journal of Functional Programming, 1992.

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, 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. Higher-Order and Symbolic Computation, pp.59-91, 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

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
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.231-253, 1999.
DOI : 10.1109/CSFW.1998.683153

S. Zdancewic and A. C. Myers, Robust declassification, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., pp.15-23, 2001.
DOI : 10.1109/CSFW.2001.930133
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.1928

S. Zdancewic and A. C. Myers, Observational determinism for concurrent program security, 16th IEEE Computer Security Foundations Workshop, 2003. Proceedings., 2003.
DOI : 10.1109/CSFW.2003.1212703

S. Zwandewic, A type system for robust declassification, Proceedings of MFPS'03, 2003.