M. Abadi, A. Banerjee, N. Heintze, and J. And-riecke, A core calculus of dependency, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.147-160, 1999.
DOI : 10.1145/292540.292555

J. Agat, Type Based Techniques for Covert Channel Elimination and Register Allocation, 2000.

T. Amtoft, S. Bandhakavi, and A. Banerjee, A logic for information flow in objectoriented programs, Principles of Programming Languages, pp.91-102, 2006.

A. W. Appel, Foundational proof-carrying code, Logic in Computer Science, p.247, 2001.
DOI : 10.1109/lics.2001.932501

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.2076

A. Askarov and A. Sabelfeld, Security-Typed Languages for Implementation of Cryptographic Protocols: A Case Study, European Symposium On Research In Computer Security, number 3679 in Lecture Notes in Computer Science, 2005.
DOI : 10.1007/11555827_12

B. E. Aydemir, A. Bohannon, M. Fairbairn, J. N. Foster, B. C. Pierce et al., Mechanized Metatheory for the Masses: The PoplMark Challenge, International Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 3603 of Lecture Notes in Computer Science, 2005.
DOI : 10.1007/11541868_4

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

G. Barthe, A. Basu, R. , and T. , Security types preserving compilation, Verification, Model Checking and Abstract Interpretation, number 2934 in Lecture Notes in Computer Science, pp.2-15, 2004.
DOI : 10.1016/j.cl.2005.05.002

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.598.8956

G. Barthe, S. Cavadini, R. , and T. , Tractable Enforcement of Declassification Policies, 2008 21st IEEE Computer Security Foundations Symposium, 2008.
DOI : 10.1109/CSF.2008.11

G. Barthe, D. Naumann, R. , and T. , Deriving an information flow checker and certifying compiler for Java, 2006 IEEE Symposium on Security and Privacy (S&P'06), 2006.
DOI : 10.1109/SP.2006.13

G. Barthe, D. Pichardie, R. , and T. , A certified lightweight non-interference Java bytecode verifier, Programming Languages and Systems: Proceedings of the 16th European Symposium on Programming, ESOP 2007, number 4421 in Lecture Notes in Computer Science, pp.125-140, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00915189

G. Barthe and T. Rezk, Non-interference for a JVM-like language, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation , TLDI '05, pp.103-112, 2005.
DOI : 10.1145/1040294.1040304

G. Barthe, T. Rezk, A. Russo, and A. Sabelfeld, Security of multithreaded programs by compilation, ACM Transactions on Information and System Security, vol.13, issue.3, 2010.
DOI : 10.1145/1805974.1805977

G. Barthe and E. Rivas, Static Enforcement of Information Flow Policies for a Concurrent JVM-like Language, Proceedings of TGC'11, volume xxxx of Lecture Notes in Computer Science, 2011.
DOI : 10.1007/978-3-642-30065-3_5

C. Bernardeschi and N. D. Francesco, Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode, Model Checking and Abstract Interpretation, pp.1-15, 2002.
DOI : 10.1007/3-540-47813-2_1

F. Besson, T. P. Jensen, D. Pichardie, and T. Turpin, Certified Result Checking for Polyhedral Analysis of Bytecode Programs, Lecture Notes in Computer Science, vol.6084, pp.253-267, 2010.
DOI : 10.1007/978-3-642-15640-3_17

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

P. Bieber, J. Cazin, P. Girard, J. Lanet, V. Wiels et al., Checking Secure Interactions of Smart Card Applets, Journal of Computer Security, vol.10, issue.4, pp.369-398, 2002.
DOI : 10.1007/10722599_1

E. Bonelli, A. B. Compagnoni, and R. Medel, Information Flow Analysis for a Typed Assembly Language with Polymorphic Stacks, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pp.37-56, 2005.
DOI : 10.1007/BFb0030629

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

S. N. Freund and J. C. Mitchell, A type system for the java bytecode language and verifier, Journal of Automated Reasoning, vol.30, pp.3-4271, 2003.

S. Genaim and F. Spoto, Information Flow Analysis for Java Bytecode, Model Checking and Abstract Interpretation, pp.346-362, 2005.
DOI : 10.1007/978-3-540-30579-8_23

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.79.5499

P. Girard, Which security policy for multiapplication smart cards?, Workshop on Smart Card Technology. USENIX Association, 1999.

C. Hammer, J. Krinke, and G. Snelting, Information flow control for java based on path conditions in dependence graphs, Symposium on Secure Software Engineering, 2006.

C. Hankin, F. Nielson, and H. R. Nielson, Principles of Program Analysis, 2005.

D. Hedin and D. Sands, Noninterference in the Presence of Non-Opaque Pointers, 19th IEEE Computer Security Foundations Workshop (CSFW'06), 2006.
DOI : 10.1109/CSFW.2006.19

S. Hunt and D. Sands, On flow-sensitive security types, Principles of Programming Languages, 2006.

N. Kobayashi and K. Shirane, Type-based information analysis for low-level languages, Asian Programming Languages and Systems Symposium, pp.302-316, 2002.

X. Leroy, Bytecode verification on Java smart cards, Software: Practice and Experience, vol.21, issue.4, pp.319-340, 2002.
DOI : 10.1002/spe.438

URL : https://hal.archives-ouvertes.fr/hal-01499944

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

R. Medel, A. B. Compagnoni, and E. Bonelli, A Typed Assembly Language for Non-interference, Italian Conference on Theoretical Computer Science, pp.360-374, 2005.
DOI : 10.1007/11560586_29

M. Montgomery and K. Krishna, Secure object sharing in Java Card, Workshop on Smart Card Technology. Usenix, 1999.

G. Morrisett, D. Walker, K. Crary, and N. Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems, vol.21, issue.3, pp.527-568, 1999.
DOI : 10.1145/319301.319345

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.6526

A. C. Myers, JFlow, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.228-241, 1999.
DOI : 10.1145/292540.292561

O. Neill, K. R. Clarkson, M. R. , C. , and S. , Information-flow security for interactive programs, Computer Security Foundations Workshop, pp.190-201, 2006.

F. Pottier and V. Simonet, Information flow inference for ML, ACM Transactions on Programming Languages and Systems, vol.25, issue.1, pp.117-158, 2003.
DOI : 10.1145/596980.596983

T. Rezk, Verification of confidentiality policies for mobile code, 2006.

E. Rose, Lightweight Bytecode Verification, Journal of Automated Reasoning, vol.31, issue.3/4, pp.3-4303, 2003.
DOI : 10.1023/B:JARS.0000021015.15794.82

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

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

D. Volpano and G. Smith, A type-based approach to program security, Theory and Practice of Software Development, 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. Yu and N. Islam, A Typed Assembly Language for Confidentiality, Programming Languages and Systems: Proceedings of the 15th European Symposium on Programming, pp.162-179, 2006.
DOI : 10.1023/A:1020843229247