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 Projects

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.

Bi-directional Type Checking

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

Kind Inference

This work proposes a solution of challenge of kind inference for datatype declarations for Haskell98 and modern Haskell.

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

Projects

  • FCore
    Research middleware compiler from System F-based languages to Java with the Imperative Functional Object encoding.