Subtyping in a Boolean Algebra of Structural Types

The Hong Kong University of Science and Technology
Department of Computer Science and Engineering


MPhil Thesis Defence


Title: "Subtyping in a Boolean Algebra of Structural Types"

By

Mr. Chun Yin CHAU


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 formal proofs for the core calculus of MLstruct, including the soundness
of the declarative system, 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:                   Friday, 14 July 2023

Time:                   4:00pm - 6:00pm

Venue:                  Room 3494
                        lifts 25/26

Committee Members:      Dr. Lionel Parreaux (Supervisor)
                        Dr. Amir Goharshady (Chairperson)
                        Prof. Shing-Chi Cheung


**** ALL are Welcome ****