M. Abadi and A. D. Gordon, Reasoning about cryptographic protocols in the spi calculus, CONCUR'97: Concurrency Theory, pp.59-73, 1997.
DOI : 10.1007/3-540-63141-0_5

J. Banâtre and C. Bryce, A security proof system for networks of communicating processes, 1993.

J. Billon, Security breaches in the JDK 1

N. S. Borenstein, Email with a mind of its own: the Safe-Tcl language for enabled mail, IFIP International Working Conference on Upper Layer Protocols, Architectures and Applications, 1994.

V. Breazu-tannen, T. Coquand, C. A. Gunter, and A. Scedrov, Inheritance as implicit coercion, Information and Computation, vol.93, issue.1, pp.172-221, 1991.
DOI : 10.1016/0890-5401(91)90055-7
URL : http://doi.org/10.1016/0890-5401(91)90055-7

K. Brunnstein, Hostile ActiveX control demonstrated, RISKS Forum, vol.18, issue.82, 1997.

L. Cardelli, S. Martini, J. C. Mitchell, and A. Scedrov, An Extension of System F with Subtyping, Information and Computation, vol.109, issue.1-2, pp.4-56, 1994.
DOI : 10.1006/inco.1994.1013

D. Dean, E. W. Felten, and D. S. Wallach, Java security: from HotJava to Netscape and beyond, Proceedings 1996 IEEE Symposium on Security and Privacy, 1996.
DOI : 10.1109/SECPRI.1996.502681
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.186.8361

D. E. Denning and P. J. Denning, Certification of programs for secure information flow, Communications of the ACM, vol.20, issue.7, pp.504-513, 1977.
DOI : 10.1145/359636.359712

D. E. Denning, A lattice model of secure information flow, Communications of the ACM, vol.19, issue.5, pp.236-242, 1976.
DOI : 10.1145/360051.360056

S. Drossopoulou and S. Eisenbach, Java is type safe ??? Probably, Proc. 11th European Conference on Object Oriented Programming, 1997.
DOI : 10.1007/BFb0053388
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.352.5159

M. Erdos, B. Hartman, and M. Mueller, Security reference model for the Java Developer's Kit 1.0.2. Java- Soft, 1996.

J. Gosling and H. Mcgilton, The Java language environment ? a white paper, JavaSoft, 1996.

N. Heinze and J. G. Riecke, The SLam calculus: programming with secrecy and integrity. Draft, available electronically, 1998.

D. Hopwood, Java security bug (applets can load native methods), RISKS Forum, vol.17, issue.83, 1996.

T. Jensen, D. L. Métayer, and T. Thorn, A formalisation of visibility and dynamic loading in Java, 1997.

X. Leroy, Polymorphic typing of an algorithmic language, 1992.
URL : https://hal.archives-ouvertes.fr/inria-00077018

R. Milner, M. Tofte, R. Harper, and D. Macqueen, The definition of Standard ML (revised), 1997.

G. Morrisett, M. Felleisen, and R. Harper, Abstract models of memory management, Proceedings of the seventh international conference on Functional programming languages and computer architecture , FPCA '95, pp.66-77, 1995.
DOI : 10.1145/224164.224182

G. C. Necula and P. Lee, Safe kernel extensions without run-time checking, Proc. Symp. Operating Systems Design and Implementation, 1996.
DOI : 10.1145/248155.238781
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.142.6054

G. C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.106-119, 1997.
DOI : 10.1145/263699.263712

T. Nipkow and D. Oheimb, is type-safe---definitely, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, 1998.
DOI : 10.1145/268946.268960
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.2452

J. Palsberg and P. O. Keefe, A type system equivalent to flow analysis, 22nd symposium Principles of Programming Languages, pp.367-378, 1995.
DOI : 10.1145/210184.210187
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.3559

J. Palsberg and P. Ørbaek, Trust in the ??-calculus, Symposium on Static Analysis '95, pp.314-329
DOI : 10.1007/3-540-60360-3_47

G. D. Plotkin, A structural approach to operational semantics, 1981.

Z. Qian, A formal specification of a large subset of Java Virtual Machine instructions. Draft, available electronically, 1997.

J. C. Reynolds, User-Defined Types and Procedural Data Structures as Complementary Approaches to Data Abstraction, Theoretical aspects of object-oriented programming, pp.13-23, 1994.
DOI : 10.1007/978-1-4612-6315-9_22

F. Rouaix, A Web navigator with applets in Caml, Proceedings of the 5th International World Wide Web Conference, pp.1365-1371, 1996.
DOI : 10.1016/0169-7552(96)00032-3

J. Talpin and P. Jouvelot, The Type and Effect Discipline, Information and Computation, vol.111, issue.2, pp.245-296, 1994.
DOI : 10.1006/inco.1994.1046
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.5309

M. Tofte, Type inference for polymorphic references. Information and Computation, 1990.
DOI : 10.1016/0890-5401(90)90018-d
URL : http://doi.org/10.1016/0890-5401(90)90018-d

D. Volpano, G. Smith, and C. Irvine, A sound type system for secure flow analysis, Journal of Computer Security, vol.4, issue.2-3, pp.1-21, 1996.
DOI : 10.3233/JCS-1996-42-304

D. Volpano and G. Smith, A type-based approach to program security Colloqium on Formal Approaches in Software Engineering Extensible security architectures for Java, Proceedings of TAPSOFT'97, 1997.

F. Yellin, Low level security in Java, Proceedings of the Fourth International World Wide Web Conference. O'Reilly, 1995.