M. Abadi and L. Cardelli, A Theory of Objects, 1996.

V. Bono and M. Bugliesi, Matching for the lambda calculus of objects, Theoretical Computer Science, vol.212, issue.1-2, pp.101-140, 1999.

V. Bono, M. Bugliesi, M. Dezani-ciancaglini, and L. Liquori, Subtyping Constraint for Incomplete Objects, Proc. of TAPSOFT/CAAP, vol.1214, pp.465-477, 1997.

V. Bono, M. Bugliesi, and L. Liquori, A Lambda Calculus of Incomplete Objects, Proc. of MFCS, vol.1113, pp.218-229, 1996.
URL : https://hal.archives-ouvertes.fr/hal-01156555

]. K. +-96, L. Bruce, G. Cardelli, B. Castagna-;-leavens, and . Pierce, The Hopkins Object Group, On Binary Methods. Theory and Practice of Object Systems, vol.1, issue.3, 1996.

V. Bono and K. Fisher, An imperative, first-order calculus with object extension, 12th European Conference, vol.1445, pp.462-497, 1998.

V. Bono and L. Liquori, A Subtyping for the Fisher-Honsell-Mitchell Lambda Calculus of Objects, Proc. of CSL, vol.933, pp.16-30, 1995.
URL : https://hal.archives-ouvertes.fr/hal-01157171

K. Bruce, L. Petersen, and A. Fiech, Subtyping Is Not a Good "Match" for Object-Oriented Languages, Proc. of ECOOP, vol.1241, pp.104-127, 1997.

K. B. Bruce, A Paradigmatic Object-Oriented Programming Language: Design, Static Typing and Semantics, Journal of Functional Programming, vol.4, issue.2, pp.127-206, 1994.

L. Cardelli, A Language with Distributed Scope. Computing System, vol.8, issue.1, pp.27-59, 1995.

G. Castagna, Covariance and contravariance: conflict without a cause, ACM Transactions on Programming Languages and Systems, vol.17, issue.3, pp.431-447, 1995.

G. Castagna, Object-Oriented Programming: A Unified Foundation, Progress in Theoretical Computer Science. Birkäuser, 1996.

T. Cohen and J. Gil, Three approaches to object evolution, Proceedings of the 7th International Conference on Principles and Practice of Programming in Java, pp.57-66, 2009.

R. Chugh, D. Herman, and R. Jhala, Dependent types for javascript, SIGPLAN Not, vol.47, issue.10, pp.587-606, 2012.

S. Drossopoulou, F. Damiani, M. Dezani-ciancaglini, and P. Giannini, Fickle : Dynamic object re-classification, ECOOP 2001 -Object-Oriented Programming, 15th European Conference, vol.2072, pp.130-149, 2001.

S. Drossopoulou, F. Damiani, M. Dezani-ciancaglini, and P. Giannini, More dynamic object reclassification: Fickle ||, ACM Trans. Program. Lang. Syst, vol.24, issue.2, pp.153-191, 2002.

F. Damiani, S. Drossopoulou, and P. Giannini, Refined effects for unanticipated object re-classification: Fickle 3, Theoretical Computer Science, 8th Italian Conference, vol.2841, pp.97-110, 2003.

P. Di-gianantonio, F. Honsell, and L. Liquori, A lambda calculus of objects with self-inflicted extension, Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA '98), pp.166-178, 1998.
URL : https://hal.archives-ouvertes.fr/hal-01154180

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

K. Fisher and J. C. Michell, Notes on Typed Object-Oriented Programming, Proc. of TACS, vol.789, pp.844-885, 1994.

K. Fisher and J. C. Mitchell, A Delegation-based Object Calculus with Subtyping, Proc. of FCT, vol.965, pp.42-61, 1995.

K. Fisher and J. C. Mitchell, On the relationship between classes, objects, and data abstraction. Theory and Practice of Object Systems, 1998.

G. Ghelli, Foundations for extensible objects with roles. Information and Computation, vol.175, pp.50-75, 2002.

T. Kamina and . Tamai, A smooth combination of role-based language and context activation, Proceedings of the Ninth Workshop on Foundation of Aspect-Oriented Languages (FOAL 2010), pp.15-24, 2010.

L. Liquori, An Extended Theory of Primitive Objects: First Order System, Proc. of ECOOP, vol.1241, pp.146-169, 1997.
URL : https://hal.archives-ouvertes.fr/hal-01154568

S. Monpratarnchai and T. Tamai, The implementation and execution framework of a role model based language, epsilonj, Ninth ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing, pp.269-276, 2008.

D. Rémy, From classes to objects via subtyping, Proc. of European Symposium on Programming, vol.1381, 1998.

J. Ressia, T. Gîrba, O. Nierstrasz, F. Perin, and L. Renggli, Talents: an environment for dynamically composing units of reuse, Softw., Pract. Exper, vol.44, issue.4, pp.413-432, 2014.

J. G. Riecke and C. Stone, Privacy via Subsumption, Electronic proceedings of FOOL-98, 1998.

M. Serrano, Wide classes, ECOOP'99 -Object-Oriented Programming, 13th European Conference, vol.1628, pp.391-415, 1999.

M. Takahashi, Parallel reductions in lambda calculus, Inf. Comput, vol.118, issue.1, pp.120-127, 1995.

J. Vouillon, Combining subsumption and binary methods: An object calculus with views, Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '01, pp.290-303, 2001.

M. Wand, neither in ? 2 ; hence, the above judgment can be written as ? 1 , t ? ?, ? 2 , ? 3 [?/t] ? ? m ? ? 2 . On the other hand, from the second hypothesis ? 1 , t ? ?, ? 2 ? ? ? we can derive ? 1 , t ? ?, ? m ? ? ? m by Lemma C.2.(ii) (Weakening) and Lemma C.5.(vii), and from the transitivity of matching (Lemma C.5.(v)), pp.37-44, 1987.

, Proposition C.8 (Types of expressions are well-formed)

, If ? e : ?, then ? ? : *

, About (Appl), the inductive hypothesis allows us to derive ? ??? : * ; this judgment can only be derived through the (T ype?Arrow) rule, whose second premise is precisely the thesis. (Rules for object terms) The thesis is trivial for the (Empty), (P re?Extend) and (Override) rules, If the last rule in ? is (Const), we derive the thesis via (T ype?Const). To address the (V ar) rule we use Lemma C.1.(ii) (Sub-derivation) and Lemma C.2.(i) (Weakening). For the (Abs) rule one applies the inductive hypothesis, Lemma C.1.(ii) (Sub-derivation), Lemma C.7.(i) (Substitution), and the (T ype?Arrow) rule

C. Theorem, Subject Reduction, ?Obj ? ) If ? e : ? and e ? e , then ? e : ?. We prove that the type is preserved by each of the four reduction rules (Beta), (Selection)

, Let the premises of (Appl) be ? (?x.e 1 ) : ??? and ? e 2 : ? for a suitable ?, The derivation ? of ? (?x.e 1 )e 2 : ? needs to terminate with a rule (Appl), deriving ? (?x.e 1 )