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.
- 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
- Union Types with Disjoint Switches - ECOOP'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 proposes a new formalization of iso-recursive subtyping and investigates its integration with various language features.
- Full Iso-Recursive Types - OOPSLA'24
- Recursive Subtyping for All - POPL'23
- A Calculus with Recursive Types, Record Concatenation and Subtyping - APLAS'22
- Revisiting Iso-Recursive Subtyping - TOPLAS
Our work improves upon bidirectional typing and proposes a new mechanized type inference technique.
- 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 unifies typing and subtyping in dependently-typed calculi, which still preserves decidable type checking.
- A Dependently Typed Calculus with Polymorphic Subtyping - SCP
- Pure Iso-Type Systems - JFP
- Unifying Typing and Subtyping - OOPSLA'17
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
Duotyping exploits the duality of intersection and union types and simplifies metatheories.