M. Abadi and L. Cardelli, A Theory of Primitive Objects: Untyped and First-Order Systems, Proc. TACS'94, Theoretical Aspects of Computing Sofware, pp.296-320, 1994.
DOI : 10.1006/inco.1996.0024

M. Abadi and L. Cardelli, A Theory of Objects. Monographs in Computer Science, 1996.

M. Boespflug and G. Burel, Coqine : Translating the calculus of inductive constructions into the ??-calculus modulo, Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01126128

M. Boespflug, Q. Carbonneaux, O. Hermant, and R. Saillard, Dedukti: a universal proof checker

K. B. Bruce, L. Cardelli, and B. C. Pierce, Comparing Object Encodings, Information and Computation, vol.155, issue.1-2, pp.108-133, 1999.
DOI : 10.1006/inco.1999.2829

A. Ciaffaglione, L. Liquori, and M. Miculan, Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts, Journal of Automated Reasoning, vol.87, issue.1, pp.1-47, 2007.
DOI : 10.1007/s10817-006-9061-y
URL : https://hal.archives-ouvertes.fr/hal-01148347

H. Cirstea, C. Kirchner, and L. Liquori, Matching Power, Proceedings of RTA'2001, 2001.
DOI : 10.1007/3-540-45127-7_8
URL : https://hal.archives-ouvertes.fr/inria-00099308

H. Cirstea, L. Liquori, and B. Wack, Rewriting Calculus with Fixpoints: Untyped and First-Order Systems, TYPES, 2003.
DOI : 10.1007/978-3-540-24849-1_10
URL : https://hal.archives-ouvertes.fr/inria-00100113

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., Maude: Specification and programming in rewriting logic. Manual distributed as documentation of the Maude system, 1999.

C. Development and T. , The Coq Reference Manual, version 8, 2012.

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, LNCS, vol.4583, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

K. Fisher, F. Honsell, and J. C. Mitchell, A lambda Calculus of Objects and Method Specialization, Nordic Journal of Computing, vol.1, pp.3-37, 1994.

N. Foster and D. Vytiniotis, A theory of featherweight java in isabelle/hol Archive of Formal Proofs, 2006.

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

M. Hedberg, A coherence theorem for martin-löf's type theory, J. Functional Programming, pp.4-8, 1998.

L. Henrio and F. Kammüller, A Mechanized Model of the Theory of Objects, Lecture Notes in Computer Science, vol.26, issue.3, pp.190-205, 2007.
DOI : 10.1007/BFb0026570
URL : https://hal.archives-ouvertes.fr/inria-00150272

L. Henrio, F. Kammüller, B. Lutz, and H. Sudhof, Locally nameless sigma calculus Archive of Formal Proofs http://afp.sf.net/entries/ Locally-Nameless-Sigma.shtml, Formal proof development, 2010.

A. Igarashi, B. Pierce, and P. Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems, vol.23, issue.3, pp.132-146, 1999.
DOI : 10.1145/503502.503505

J. Mackay, H. Mehnert, A. Potanin, L. Groves, and N. Cameron, Encoding Featherweight Java with assignment and immutability using the Coq proof assistant, Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs, FTfJP '12, pp.11-19, 2012.
DOI : 10.1145/2318202.2318206

. Müller, Confluence of the lambda calculus with left-linear algebraic rewriting, Information Processing Letters, vol.41, issue.6, pp.293-299, 1992.
DOI : 10.1016/0020-0190(92)90155-O

F. Pfenning and C. Elliott, Higher-order abstract syntax 26 Frank Pfenning and Carsten Schurmann. System description: Twelf ? a meta-logical framework for deductive systems, Programming Language Design and Implementation Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pp.202-206, 1988.

C. Benjamin, D. N. Pierce, and . Turner, Simple type-theoretic foundations for objectoriented programming, Journal of Functional Programming, vol.4, issue.2, pp.207-247, 1994.

J. Zwanenburg, Object-Oriented Concepts and Proof Rules: Formalization in Type Theory and Implementation in Yarrow, 1999.