Proof of the Principal Type Property for System O Martin Wehr and Martin Odersky Technical Report 1996-16 of University of Karlsruhe We study a minimal extension of the Hindley/Milner system that supports overloading and polymorphic records. We also show that every typable term in this system has a principal type and give an algorithm to reconstruct that type. We give the proofs for termination, soundness and correctness for the constrained unification and the type reconstruction algorithm.