Subtyping in a boolean algebra of structural types

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.

Date of Award	2023
Original language	English
Awarding Institution	The Hong Kong University of Science and Technology
Supervisor	Lionel PARREAUX (Supervisor)