HKU PL Group
We are a group of programming language researchers who study topics about functional language design, type theory, compilers and program analysis.
The University of Hong Kong
Highlight
Disjoint Intersection Types
Calculi about disjoint intersection types enable an highly modular and compositional programming style that addresses the Expression Problem naturally, and allows for a much more dynamic form of inheritance.
Compositional Programming
Those works present a novel modular programming style.
-
Typed First-Class Traits ECOOP 18
-
Compositional Programming TOPLAS
Gradual Typing
This work presents a generalized definition of consistent subtyping that works for polymorphic types.
-
Consistent Subtyping for All TOPLAS
Dependent Types
Those works propose a unified syntax that accounts for types and terms which still preserves decidable type-checking.
Higher-Ranked Polymorphism
This paper provides the first mechanized formalization of type inference for higher-ranked polymorphism.
Kind Inference
This work proposes a solution of challenge of kind inference for datatype declarations for Haskell98 and modern Haskell.
-
Kind Inference for Datatypes POPL 20
Subtyping for Iso-recursive Types
A new iso-recursive subtyping formulation which takes advantage over other designs on both theoretical side and implementation side.
-
Revisiting Iso-Recursive Subtyping OOPSLA 20
Bi-directional Type Checking
This paper presents a variant of bi-directional type checking where the type information flows from arguments to functions.
-
Let Arguments go First ESOP 18
Intersection and Union Types
This paper proposes a novel methodology for designing subtyping relations that exploits duality between intersection types and union types.
Type-directed Operational Semantics
Type-directed operational semantics(TDOS) is a variant of small-step operational semantics. In TDOS, type annotations become operationally relevant and can affect the result of a program.
Members
Faculty
-
Bruno C. d. S. Oliveira Associate Professor
Current Members
-
Xuejing (Snow) Huang PhD student
-
Yaoda Zhou PhD student
-
Baber Rehman PhD student
-
Mingqi (Alvin) Xue PhD student
-
Yaozhu Sun PhD student
-
Wenjia Ye PhD student
-
Xu Xue MPhil student
-
Chen Cui PhD student
-
Jinhao Tan PhD student
-
Shengyi Jiang PhD student
-
Litao (Tony) Zhou PhD student (incoming)
Alumni
Seminar
-
Generalizing Worklist-based Inference for Dependent Types
Oct 29, 2021
The worklist style inference algorithm is marvelous legacy left by no other than the great Dr. Jimmy Zhao, which handles the problem of type inference for a system with higher-ranked... -
Revisiting Occurrence Typing: Global Context and Disjointness
Oct 22, 2021
Flow typing or occurrence typing specializes the type of an expression in a type-case analysis. It has been implemented in some modern programming languages including Ceylon, Typescript, Flow and Racket... -
Simplifying Type Inference
Sep 17, 2021
To extend the formalization of type inference with various practical features, including bounded quantification and union and intersection types, a minimal, unified and scalable metatheory is firstly needed. In this... -
On the Deduction Theorem and Subtyping Relations
Aug 31, 2021
-
Union Types with Disjoint Switches
Aug 17, 2021
Union types allow expressing terms with alternative types, and are nowadays a common feature in many modern programming languages. This work investigates a formulation of union types, inspired by the...
