M. Abadi and L. Cardelli, A theory of objects, 1996.
DOI : 10.1007/978-1-4419-8598-9

M. Abadi and K. Leino, A logic of object-oriented programs, Proc. of TAPSOFT, 1997.

G. Barthe, P. Courtieu, G. Dufay, and S. M. De-sousa, Tool-Assisted Specification and Verification of the JavaCard Platform, Proc. of AMAST, 2002.
DOI : 10.1007/3-540-45719-4_4

Y. Bertot, A certified compiler for an imperative language, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00073199

Y. Bertot, Formalizing a JVML Verifier for Initialization in a Theorem Prover, Proc. of CAV, 2001.
DOI : 10.1007/3-540-44585-4_3

R. Burstall and F. Honsell, Operational semantics in a natural deduction setting, Logical Frameworks, 1990.
DOI : 10.1017/CBO9780511569807.009

L. Cardelli, Obliq: A Language with Distributed Scope, Computing Systems, 1995.
DOI : 10.1145/199448.199516
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.187.4687

A. Ciaffaglione, Certified reasoning on Real Numbers and Objects in Co-inductive Type Theory, Dipartimento di Matematica e Informatica, 2003.

A. Ciaffaglione, L. Liquori, and M. Miculan, On the formalization of imperative objectbased calculi in (co)inductive type theories, 2003.

A. Ciaffaglione, L. Liquori, and M. Miculan, The Web Appendix of this paper, 2003.

J. Despeyroux, Proof of translation in natural semantics, Proc. of LICS, 1986.
URL : https://hal.archives-ouvertes.fr/inria-00076040

J. Despeyroux, A. Felty, and A. Hirschowitz, Higher-order syntax in Coq, Proc. of TLCA, LNCS 905, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00074124

K. Fisher, F. Honsell, and J. Mitchell, A lambda calculus of objects and method specialization, Nordic Journal of Computing, 1994.

E. Giménez, Codifying guarded recursion definitions with recursive schemes, Proc. of TYPES, 1995.

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, 1993.
DOI : 10.1145/138027.138060
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.5854

F. Honsell, M. Miculan, and I. Scagnetto, An axiomatic approach to metareasoning on systems in higher-order abstract syntax, Proc. of ICALP, 2001.

M. Huisman, Reasoning about Java programs in higher order logic with PVS and Isabelle, 2001.

G. Kahn, Natural semantics, Proc. of TACS, 1987.
DOI : 10.1007/BFb0039592
URL : https://hal.archives-ouvertes.fr/inria-00075953

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

O. Laurent, Sémantique Naturelle et Coq : vers la spécification et les preuves sur les langagesà langages`langagesà objets, 1997.

M. Miculan, The expressive power of Structural Operational Semantics with explicit assumptions
DOI : 10.1007/3-540-58085-9_80

M. Miculan, Encoding Logical Theories of Programs, 1997.

F. Pfenning and C. Elliott, Higher-order abstract syntax, Proc. of ACM SIGPLAN, 1988.

I. Scagnetto, Reasoning about Names In Higher-Order Abstract Syntax, Dipartimento di Matematica e Informatica, 2002.

M. Strecker, Formal Verification of a Java Compiler in Isabelle, Proc. of CADE, 2002.
DOI : 10.1007/3-540-45620-1_5

H. Tews, A case study in coalgebraic specification: memory management in the FIASCO microkernel, 2000.

J. Van-den-berg, B. Jacobs, and E. Poll, Formal specification and verification of JavaCard's application identifier class, Proc. of the JavaCard 2000 Workshop, 2001.