T. If, then m ? meth(TA) if and only if altlook(m, TA) = fail. Proof. By induction on the derivation of altlook

T. , ?. ?ta, and ?. Ta, altlook(m, TA i ) = fail. Thus we have, by induction hypothesis altlook(m, TA) = fail ??

T. If, ) is a function

T. , T. , ?. ·. Ta, and T. , ? If m ? ?TA, then, there is a unique TA i ? TA where altlook(m, TA i ) = fail. ? If m ? ?TA, then, since TA is well-typed, the rule (Tr·Ok) enforces that m ? ?TA. Then, for all TA i ? TA, we have m ? meth(TA i ) ? m in TA i n in TA 1 . Moreover, we know that n ? meth(TA 1 ), by Lemma C.1 (Non Virtual Paths), which means that there is at least one altlook(n, TA 1 ) = B n (B x){. . .} which is derivable, by Lemma C.4 (meth Soundness). Thus, altlook(m, TA i ) = B m (B x){. . .} is derivable for all TA i such that m ? meth, ATr·Inh) If tlook i ) is a function which ensures they are all equal. Which obviously gives the result

?. ?. If, ?. , ?. , ?. ?. For-some, and D. Proof, The proof is as in, 2001.

. Proofigarashi, The proof is almost the same as in There is a very little to add, just remember that we need Theorem C.1 (Conflict Resolution) to achieve the full proof, 2001.

. Proof, As in [Igarashi et al. 2001], this proof is just similar to the Subject Reduction proof

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

E. Allen, D. Chase, V. Luchangco, J. Maessen, S. Ryu et al., The Fortress Language Specification, version 0, 2005.

D. Ancona, G. Lagorio, and E. Zucca, Jam---designing a Java extension with mixins, ACM Transactions on Programming Languages and Systems, vol.25, issue.5, pp.641-712, 2003.
DOI : 10.1145/937563.937567

D. Ancona and E. Zucca, A calculus of module systems, Journal of Functional Programming, vol.12, issue.02, pp.91-132, 2002.
DOI : 10.1017/S0956796801004257

D. Ancona and E. Zucca, A theory of mixin modules: algebraic laws and reduction semantics, Mathematical Structures in Computer Science, vol.12, issue.06, pp.701-737, 2002.
DOI : 10.1017/S0960129502003687

V. Bono, M. Bugliesi, M. Dezani-ciancaglini, and L. Liquori, Subtyping constraints for incomplete objects, Proc. of TAPSOFT/CAAP, pp.465-477, 1997.
DOI : 10.1007/BFb0030619
URL : https://hal.archives-ouvertes.fr/hal-01154622

V. Bono, A. Patel, and V. Shmatikov, A Core Calculus of Classes and Mixins, Proc. of ECOOP, 1999.
DOI : 10.1007/3-540-48743-3_3

G. Bracha, The Programming Language Jigsaw: Mixins, Modularity and Multiple Inheritance, 1992.

G. Bracha and W. R. Cook, Mixin-based inheritance, Proc. of OOPSLA/ECOOP. SIGPLAN Notices, pp.303-311, 1990.
DOI : 10.1145/97946.97982
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.156.4510

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

D. Gianantonio, P. Honsell, F. Liquori, and L. , A Lambda Calculus of Objects with Self-inflicted Extension, Proc. of OOPSLA, pp.166-178, 1998.
URL : https://hal.archives-ouvertes.fr/hal-01154180

S. Ducasse, O. Nierstrasz, N. Schärli, R. Wuyts, and A. P. Black, Traits, ACM Transactions on Programming Languages and Systems, vol.28, issue.2, pp.331-388, 2006.
DOI : 10.1145/1119479.1119483
URL : https://hal.archives-ouvertes.fr/inria-00403568

D. Duggan and C. Sourelis, Mixin modules, Proc. of ICFP. SIGPLAN Notices, pp.262-273, 1996.
DOI : 10.1145/232627.232654

R. B. Findler and M. Flatt, Modular Object-Oriented Programming with Units and Mixins, Proc. of ICFP. SIGPLAN Notices, pp.94-104, 1998.

K. Fisher and J. Reppy, Statically Typed Traitspdf. The early version " A Typed Calculus of Traits, 2004.

M. Flatt and M. Felleisen, Units: Cool Modules for HOT Languages, Proc. of PLDI. SIGPLAN Notices, pp.236-248, 1998.

M. Flatt, S. Krishnamurthi, and M. Felleisen, Classes and mixins, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.171-183, 1998.
DOI : 10.1145/268946.268961

A. Goldberg and D. Robson, Smalltalk-80: the Language and its Implementation, 1983.

T. Hirschowitz, X. Leroy, W. , and J. B. , Call-by-Value Mixin Modules, Proc. of ESOP, pp.64-78, 2004.
DOI : 10.1007/978-3-540-24725-8_6
URL : https://hal.archives-ouvertes.fr/hal-00310119

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.396-450, 2001.
DOI : 10.1145/503502.503505

G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. V. Lopes et al., Aspect-Oriented Programming, Proc. of ECOOP, pp.220-242, 1997.

L. Liquori, An extended Theory of Primitive Objects: First order system, Proc. of ECOOP, pp.146-169, 1997.
DOI : 10.1007/BFb0053378
URL : https://hal.archives-ouvertes.fr/hal-01154568

L. Liquori, On object extension, Proc. of ECOOP, pp.498-552, 1998.
DOI : 10.1007/BFb0054105
URL : https://hal.archives-ouvertes.fr/hal-01154560

L. Liquori and A. Spiwack, Featherweight-Trait Java : A Trait-based Extension for FJ, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00070751

L. Liquori and A. Spiwack, Extending FeatherTrait Java with Interfaces. Theoretical Computer Science, 2007.
DOI : 10.1016/j.tcs.2008.01.051
URL : https://hal.archives-ouvertes.fr/inria-00432540

M. Flatt, S. Krishnamurthi, and M. F. , Classes and mixins, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.171-183, 1998.
DOI : 10.1145/268946.268961

M. Mezini, Towards Variational Object-Oriented Programming: The Rondo Model, 2002.

. Microsoft, The C# Home Page, 2007.

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

M. Team and T. , The Moby Home Page, 2007.

O. Nierstrasz, S. Ducasse, and N. Schärli, Flattening Traits., The Journal of Object Technology, vol.5, issue.4, pp.129-148, 2006.
DOI : 10.5381/jot.2006.5.4.a4

P. J. Quitslung, Java Traits ? Improving Opportunities for Reuse, 2004.

S. Team and T. , The Scala Home Page, 2007.

N. Schärli, S. Ducasse, O. Nierstrasz, and A. Black, Traits: Composable Units of Behaviour, Proc. of ECOOP, pp.248-274, 2003.
DOI : 10.1007/978-3-540-45070-2_12

C. Smith and S. Drossopoulou, Chai: Typed Traits in Java, Proc. of ECOOP, pp.453-478, 2005.

A. Snyder, Inheritance and the Development of Encapsulated Software Systems, Research Directions in Object-Oriented Programming, pp.165-188, 1987.

B. Stroustrup, The C++ Programming Language, Ch. 15, Third Ed, Java Technology, 1997.

D. Ungar, R. Smith, and B. , Self: The Power of Simplicity, Proc. of OOPSLA, pp.227-241, 1987.

J. B. Wells and R. Vestergaard, Equational Reasoning for Linking with First-Class Primitive Modules, Proc. of ESOP, pp.412-428, 2000.
DOI : 10.1007/3-540-46425-5_27