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.
- 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.
- 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.
- Recursive Subtyping for All POPL'23
- A Calculus with Recursive Types, Record Concatenation and Subtyping APLAS'22
- Revisiting Iso-Recursive Subtyping TOPLAS
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.
- 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.
- Pragmatic Gradual Polymorphism with References ESOP'23
- Type-Directed Operational Semantics for Gradual Typing ECOOP'21
- Consistent Subtyping for All TOPLAS
Duotyping exploits the duality of intersection and union types and simplifies metatheories.