Location via proxy:   
[Report a bug]   [Manage cookies]                
HKU PL Group

The Programming Languages Group at The University of Hong Kong (HKU) conducts research on programming language design and implementation, especially about type systems.

Research Highlights

This line of work introduces new designs for iso-recursive subtyping and explores their integration with various language features.

This line of work focuses on improving bidirectional typing, type inference, and formalization of subtyping.

This line of work explores the duality between intersection and union types and aims to simplify their metatheories.

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.

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

This line of work unifies typing and subtyping in dependently-typed calculi, while preserving decidable type checking.

This line of work investigates techniques for enhancing modularity in software development, with a particular emphasis on object algebras.

The following works were carried out in close partnership with external collaborators. We are very thankful for their insights, generosity, and the opportunity to work together.