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
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.
Those works present a novel modular programming style.
This work presents a generalized definition of consistent subtyping that works for polymorphic types.
Consistent Subtyping for All TOPLAS
Those works propose a unified syntax that accounts for types and terms which still preserves decidable type-checking.
This paper provides the first mechanized formalization of type inference for higher-ranked polymorphism.
This work proposes a solution of challenge of kind inference for datatype declarations for Haskell98 and modern Haskell.
Kind Inference for Datatypes POPL 20
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
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
This paper proposes a novel methodology for designing subtyping relations that exploits duality between intersection types and union types.
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.
Bruno C. d. S. Oliveira Associate Professor
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)
Type Directed Operational Semantics for Gradual Typing
Mar 30, 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...
Polymorphic Subtyping and Dependent Types
Jan 19, 2021
Abstract: The polymorphic subtyping relation, which captures the more-general-than relation between polymorphic and monomorphic types, is one of the main ways modern functional programming languages handles parametric polymorphisms (generic types)...
Zord Meets WebAssembly: Compiling a Functional Language
Nov 10, 2020
Type Inference with Rank-1 Restriction
Nov 3, 2020
Type Inference plays an important role in modern programming language design, as the functional programming style is accepted by more and more programmers. Unfortunately, full type inference on System F...
Direct Gradually Typed Lambda Calculus with Merge Operator
Sep 22, 2020
Because dynamic typing and static typing have their own advantages. For example, static typing detects the error early but the dynamic typing is more flexible. It is hard to chose...