Abstract
MLstruct is a language that combines intersection and union types with principal type inference, allowing programmers to leverage the powerful expressiveness of these types without the overhead of type annotations, while retaining the safety guarantees of statically typed languages. We present the formal proofs for the core calculus of MLstruct, including the soundness of the declarative system, and the soundness and completeness of the type inference algorithm. With this work, we hope to establish the sound foundation of MLstruct, upon which the powerful language MLscript is built, preparing it for wider adoption.