The programming languages group at the University of Hong Kong conducts research on programming language design and implementation, especially about type systems.
Research Highlights
Our work proposes new designs for iso-recursive subtyping and investigates its integration with various language features.
- Recursive Subtyping for All - JFP
- QuickSub: Efficient Iso-Recursive Subtyping - POPL'25
- Full Iso-Recursive Types - OOPSLA'24
- A Calculus with Recursive Types, Record Concatenation and Subtyping - APLAS'22
- Revisiting Iso-Recursive Subtyping - TOPLAS
Our work improves upon bidirectional typing and proposes new mechanized type inference techniques.
- Bidirectional Higher-Rank Polymorphism with Intersection and Union Types - POPL'25
- Contextual Typing - ICFP'24
- Greedy Implicit Bounded Quantification - OOPSLA'23
- Elementary Type Inference - ECOOP'22
- A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference - ICFP'19
- Let Arguments Go First - ESOP'18
Our work explores the duality of intersection and union types and simplifies metatheories.
- Named Arguments as Intersections, Optional Arguments as Unions - ESOP'25
- Disjoint Polymorphism with Intersection and Union Types - FTfJP'24
- Union Types with Disjoint Switches - ECOOP'22
- Distributing Intersection and Union Types with Splits and Duality (Functional Pearl) - ICFP'21
- The Duality of Subtyping - ECOOP'20
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.
- A Case for First-Class Environments - OOPSLA'24
- Dependent Merges and First-Class Environments - ECOOP'23
- A Bowtie for a Beast - POPL'23
- Making a Type Difference - POPL'23
- Applicative Intersection Types - APLAS'22
- Direct Foundations for Compositional Programming - ECOOP'22
- Taming the Merge Operator - JFP
- Row and Bounded Polymorphism via Disjoint Polymorphism - ECOOP'20
- Distributive Disjoint Polymorphism for Compositional Programming - ESOP'19
- The Essence of Nested Composition - ECOOP'18
- Disjoint Polymorphism - ESOP'17
- Disjoint Intersection Types - ICFP'16
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.
- Imperative Compositional Programming - OOPSLA'24
- Compositional Embeddings of Domain-Specific Languages - OOPSLA'22
- Compositional Programming - TOPLAS
- Shallow EDSLs and Object-Oriented Programming - <Programming>'19
- Typed First-Class Traits - ECOOP'18
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.
- Merging Gradual Typing - OOPSLA'24
- Type-Directed Operational Semantics for Gradual Typing - JFP
- Pragmatic Gradual Polymorphism with References - ESOP'23
- Consistent Subtyping for All - TOPLAS
Our work unifies typing and subtyping in dependently-typed calculi, which still preserves decidable type checking.