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 ,
A Theory of Primitive Objects: Untyped and First-Order Systems, Information and Computation, vol.125, issue.2 ,
DOI : 10.1006/inco.1996.0024
A Theory of Objects, 1996. ,
DOI : 10.1007/978-1-4419-8598-9
Object calculi with dynamic messages, FOOL'6 Workshop on Foundation of Object Oriented Languages, 1999. ,
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
A Lambda Calculus of Objects and Method Specialization Bounded Polymorphism for Extensible Object, Course DEA: Typage et programmation, pp.3-37, 1994. ,
Description Abstraite des Systèmes de Réécriture, 1996. ,
Abstract, Journal of Functional Programming, 1991. ,
DOI : 10.1016/S0019-9958(82)80087-9
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
Synthèse de types en présence de sous-typage: de la théoriè a la pratique, 1998. ,
Types et Contraintes Mémoire d'habilitationàhabilitation`habilitationà diriger des recherches, 2004. ,
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