Boolean Algebraic Subtyping

PhD Qualifying Examination


Title: "Boolean Algebraic Subtyping"

by

Mr. Chun Yin CHAU


Abstract:

Union and intersection types have been prevalent in modern programming 
languages like Scala 3 and TypeScript, enabling the programmer to express 
rich types in their programs. Efficient principal type inference in the 
presence of such types, despite being crucial for a seamless programming 
experience, has historically been challenging.

In this survey, we review the various approaches to solving the problem, with 
an emphasis on contrasting their interpretations of subtyping, including type 
elaboration, set-theoretic semantics, algebraic subtyping, and 
Boolean-algebraic subtyping. We also give an overview on their soundness 
proofs, with an emphasis on contrasting the semantic proof of 
Boolean-algebraic subtyping with its syntactic variant. Finally, we compare 
the type inference algorithms for the various systems.


Date:                   Thursday, 25 September 2025

Time:                   3:00pm - 5:00pm

Venue:                  Room 5501
                        Lifts 25/26

Committee Members:      Dr. Lionel Parreaux (Supervisor)
                        Prof. Charles Zhang (Chairperson)
                        Dr. Jiasi Shen