. Proof, The proof from Mitchell paper seem to fit this adaptation well; it relies in propagate and simplify constraints; it is quite technical and it is currently being checked. A bit of care must be devoted in studying complexity of the algorithm

R. Abadi and L. Cardelli, A Theory of Primitive Objects: Untyped and First-Order Systems, Information and Computation, vol.125, issue.2
DOI : 10.1006/inco.1996.0024

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

M. Bugliesi and S. Crafa, Object calculi with dynamic messages, FOOL'6 Workshop on Foundation of Object Oriented Languages, 1999.

L. Damas and R. Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982.
DOI : 10.1145/582153.582176

K. Fisher, F. Honsell, J. C. Mitchellliq97-]-l, . Liquorilp-]-x, F. Leroy et al., A Lambda Calculus of Objects and Method Specialization Bounded Polymorphism for Extensible Object, Course DEA: Typage et programmation, pp.3-37, 1994.

P. Es, Description Abstraite des Systèmes de Réécriture, 1996.

J. C. Mitchell, Abstract, Journal of Functional Programming, 1991.
DOI : 10.1016/S0019-9958(82)80087-9

M. Müller and S. Nishimura, TYPE INFERENCE FOR FIRST-CLASS MESSAGES WITH FEATURE CONSTRAINTS, International Journal of Foundations of Computer Science, vol.11, issue.01, pp.29-63, 2000.
DOI : 10.1142/S0129054100000041

F. Pottier, Synthèse de types en présence de sous-typage: de la théoriè a la pratique, 1998.

F. Pottier, Types et Contraintes Mémoire d'habilitationàhabilitation`habilitationà diriger des recherches, 2004.

J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-49, 1965.
DOI : 10.1145/321250.321253