M. Abadi, Secrecy by typing in security protocols, Journal of the ACM, vol.46, issue.5, pp.749-786, 1999.
DOI : 10.1145/324133.324266

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

M. Abadi, A. Banerjee, N. Heintze, and J. G. 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

M. Abadi and B. Blanchet, Secrecy Types for Asymmetric Communication, Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures, pp.25-41, 2001.
DOI : 10.1007/3-540-45315-6_2

URL : http://doi.org/10.1016/s0304-3975(02)00863-0

M. Abadi and A. D. Gordon, A calculus for cryptographic protocols, Proceedings of the 4th ACM conference on Computer and communications security , CCS '97, pp.1-70, 1999.
DOI : 10.1145/266420.266432

R. Anderson and R. Needham, Programming Satan's computer. In Computer Science Today: Recent Trends and Developments, number 1000 in Lecture Notes in Computer Science, pp.426-441, 1995.

F. Besson, T. De-grenier-de-latour, and T. Jensen, Secure calling contexts for stack inspection, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '02, pp.76-87, 2002.
DOI : 10.1145/571157.571166

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

L. Cardelli, Type systems The Computer Science and Engineering Handbook, 1997.

D. Caromel, L. Henrio, and B. Serpette, Context Inference for Static Analysis of Java Card Object Sharing, Proceedings e-Smart 2001, 2001.
DOI : 10.1007/3-540-45418-7_5

Z. Chen, Java Card Technology for Smart Cards: Architecture and Programmer's Guide. The Java Series, 2000.

G. Chugunov, L. Fredlund, and D. Gurov, Model checking multiapplet Java Card applications, Smart Card Research and Advanced Applications Conference (CARDIS'02), 2002.

T. Colcombet and P. Fradet, Enforcing trace properties by program transformation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, pp.54-66, 2000.
DOI : 10.1145/325694.325703

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

K. Crary and J. C. Vanderwaart, An expressive, scalable type theory for certified code, International Conference on Functional Programming, 2002.
DOI : 10.1145/583852.581497

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

D. Deville and G. Grimaud, Building an " impossible " verifier on a Java Card, USENIX Workshop on Industrial Experiences with Systems Software (WIESS'02), 2002.

U. Erlingsson and F. B. Schneider, IRM enforcement of Java stack inspection, Proceeding 2000 IEEE Symposium on Security and Privacy. S&P 2000, 2000.
DOI : 10.1109/SECPRI.2000.848461

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

M. Gasser, Building a secure computer system, 1988.

L. Gong, Inside Java 2 platform security: architecture, API design, and implementation . The Java Series, 1999.

J. A. Gosling, Java intermediate bytecodes, Proc. ACM SIGPLAN Workshop on Intermediate Representations, pp.111-118, 1995.
DOI : 10.1145/202530.202541

H. Pieter, . Hartel, A. V. Luc, and . Moreau, Formalizing the safety of Java, the Java virtual machine and Java Card, ACM Computing Surveys, vol.33, issue.4, pp.517-558, 2001.

N. Heintze and J. G. Riecke, The SLam calculus, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.365-377, 1998.
DOI : 10.1145/268946.268976

G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. V. Lopes et al., Aspect-oriented programming, European Conference on Object-Oriented Programming (ECOOP'97), number 1241 in Lecture Notes in Computer Science, 1997.

C. Paul and . Kocher, Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems, Proceedings Crypto '96, number 1109 in Lecture Notes in Computer Science, pp.104-113, 1996.

M. Kuhn, Tamper resistance -a cautionary note, USENIX Workshop on Electronic Commerce proceedings, pp.1-11, 1996.

M. Kuhn, Design principles for tamper-resistant smartcard processors, USENIX Workshop on Smartcard Technology proceedings, 1999.

X. Leroy, Java Bytecode Verification: An Overview, Computer Aided Verification, pp.265-285, 2001.
DOI : 10.1007/3-540-44585-4_26

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

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

X. Leroy and F. Rouaix, Security Properties of Typed Applets, Secure Internet Programming ? Security issues for Mobile and Distributed Objects, pp.147-182, 1999.
DOI : 10.1007/3-540-48749-2_7

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

T. Lindholm and F. Yellin, The Java Virtual Machine Specification. The Java Series, 1999.

S. Loureiro, L. Bussard, and Y. Roudier, Extending tamper-proof hardware security to untrusted execution environments, USENIX Smart Card Research and Advanced Application Conference (CARDIS'02), 2002.

G. Morrisett, K. Crary, N. Glew, and D. Walker, Stack-based typed assembly language, Journal of Functional Programming, vol.12, issue.1, pp.43-88, 2002.
DOI : 10.1007/bfb0055511

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

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.528-569, 1999.
DOI : 10.1145/268946.268954

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

C. George and . Necula, Proof-carrying code, 24th symposium Principles of Programming Languages, pp.106-119, 1997.

C. George, P. Necula, and . Lee, Safe, untrusted agents using proof-carrying code, Mobile Agents and Security, pp.61-91, 1997.

F. Pottier and S. Conchon, Information flow inference for free, International Conference on Functional Programming, pp.46-57, 2000.
DOI : 10.1145/357766.351245

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

F. Pottier and V. Simonet, Information flow inference for ML, 29th symposium Principles of Programming Languages, pp.319-330, 2002.
DOI : 10.1145/565816.503302

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

F. Pottier, C. Skalka, and S. Smith, A systematic approach to static access control, Proceedings of the 10th European Symposium on Programming, pp.30-45, 2001.
DOI : 10.1145/1057387.1057392

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

F. B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security, vol.2, issue.4, 2000.
DOI : 10.1109/fits.2003.1264930

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

Z. Shao, B. Saha, V. Trifonov, and N. Papaspyrou, A type system for certified binaries, 29th symposium Principles of Programming Languages, pp.217-232, 2002.
DOI : 10.1145/565816.503293

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

W. Sean, S. Smith, and . Weingart, Building a high-performance, programmable secure coprocessor, IBM Research, 1998.

P. Thiemann, Enforcing security properties by type specialization, European Symposium on Programming, 2001.
DOI : 10.1007/3-540-45309-1_5

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

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

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

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

URL : http://doi.org/10.3233/jcs-1996-42-304

R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham, Efficient software-based fault isolation, ACM SIGOPS Operating Systems Review, vol.27, issue.5, pp.203-216, 1993.
DOI : 10.1145/173668.168635

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

D. Walker, A type system for expressive security policies, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, pp.254-267, 2000.
DOI : 10.1145/325694.325728

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

D. S. Wallach, E. W. Felten, and A. W. Appel, The security architecture formerly known as stack inspection: A security mechanism for language-based systems, ACM Transactions on Software Engineering and Methodology, vol.9, issue.4, 2000.

H. Xi and R. Harper, A dependently typed assembly language, International Conference on Functional Programming '01, pp.169-180, 2001.
DOI : 10.1145/507656.507657

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

H. Xi and F. Pfenning, Eliminating array bound checking through dependent types, Programming Language Design and Implementation 1998, pp.249-257, 1998.
DOI : 10.1145/277650.277732

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