The programming languages group at the University of Hong Kong conducts research on programming language design and implementation, especially about type systems.

Research Highlights

This line of work explores the theoretical aspects of the merge operator and develops novel notions such as disjoint intersection types, disjoint polymorphism, nested composition, disjoint switches, type difference, dependent merges, and type-directed operational semantics.

Compositional Programming, based on calculi with the merge operator and first-class traits, is a new statically-typed programming paradigm that addresses challenges like the Expression Problem and improves the modularity and extensibility of domain-specific languages.

Our work proposes a new formalization of iso-recursive subtyping and investigates its integration with various language features.

Our work proposes a variant of bidirectional typing and a new mechanized proof technique, both of which give solutions to type inference for higher-ranked polymorphism.

Our work unifies typing and subtyping in dependently-typed calculi, which still preserves decidable type checking.

Our work presents a generalized definition of consistent subtyping in gradually-typed calculi with implicit polymorphism and applies type-directed operational semantics to gradual typing.

Duotyping exploits the duality of intersection and union types and simplifies metatheories.