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

Highlight

Disjoint Intersection Types

These are a series of works about disjoint intersection types. By supporting a merge operator, the calculi with disjoint intersection types provide general mechanisms that can subsume various other features. Such calculi can also encode highly dynamic forms of object composition, which capture common programming patterns in dynamically typed languages (such as JavaScript) in a fully statically typed manner.

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

This work reviews the Amber rules, a widely used subtyping rules for iso-recursive types and proposes a new iso-recursive subtyping rules. The novel design of double unfolding rules 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.

Members

Faculty

Current Members

Almuni

Seminar

Gallery

  • missing
    Lab dinner 2019