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 Members Seminar Gallery


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.

Gradual Typing

This work presents a generalized definition of consistent subtyping that works for polymorphic types.

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.

Subtyping for Iso-recursive Types

A new iso-recursive subtyping formulation which takes advantage over other designs on both theoretical side and implementation side.

Bi-directional Type Checking

This paper presents a variant of bi-directional type checking where the type information flows from arguments to functions.

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.


  • Revisiting type disjointness
    Jul 27, 2021
    In this problem session, we will go over the existing definitions of type disjointness and discuss an alternative approach proposed by Jimmy.

  • Applicative Intersection Types
    Jul 6, 2021
    λi adopts a classical bidirectional type checking and gives rise to many type annotations in the process of function application. In this seminar talk, I will give an introduction to...

  • Type-Directed Operational Semantics for Gradual Typing
    Jun 22, 2021
    The semantics of gradually typed languages is typically given indirectly via an elaboration into a cast calculus. This contrasts with more conventional formulations of programming language semantics, where the semantics...

  • A Dependently Typed Calculus with Polymorphic Subtyping
    Jun 22, 2021
    A polymorphic subtyping relation, which relates more general types to more specific ones, is at the core of many modern functional languages. As those languages start moving towards dependently typed...

  • Revisiting Iso-recrusive Subtyping
    May 25, 2021
    The Amber rules are well-known and widely used for subtyping iso-recursive types. They were first briefly and informally introduced in 1985 by Cardelli in a manuscript describing the Amber language....


  • missing
    Lab dinner 2019