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
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.
Disjoint Intersection Types ICFP 16
Disjoint Polymorphism ESOP 17
The Essence of Nested Composition ECOOP 18
Distributive Disjoint Polymorphism for Compositional Programming ESOP 19
A Type-Directed Operational Semantics for a Calculus with a Merge Operator ECOOP 20
Row and Bounded Polymorphism via Disjoint Polymorphism ECOOP 20
Those works present a novel modular programming style.
Typed First-Class Traits ECOOP 18
Shallow EDSLs and Object-Oriented Programming: Beyond Simple Compositionality The Programming Journal
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.
Unifying Typing and Subtyping OOPSLA 17
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
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.
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.
The Duality of Subtyping ECOOP 20
Bruno C. d. S. Oliveira Associate Professor
Weixin Zhang PhD student
Ningning Xie PhD student
Jimmy, Jinxu Zhao PhD student
Snow, Xuejing Huang PhD student
Yaoda Zhou PhD student
Baber Rehman PhD student
Alvin, Mingqi Xue PhD student
Yaozhu Sun PhD student
Wenjia Ye PhD student
Xu Xue MPhil student
Tomas Tauber PhD
Jeremy, Xuan Bi PhD
Haoyuan Zhang PhD
Huang Li MPhil
Revisiting Merges and Disjointness
Jun 23, 2020
Kind Inference For Datatypes
Jan 20, 2020
Abstract In recent years, languages like Haskell have seen a dramatic surge of new features that significantly extends the expressive...
Towards Language Support For Object Algebras
Nov 4, 2019
Abstract Object Algebras are a simple solution to the Expression Problem for mainstream object-oriented languages. However, it is still cumbersome...
Elaboration For The Worklist Algorithm
Oct 28, 2019
Type Inference For Object Oriented Programming With Higher Ranked Polymorphism
Sep 16, 2019
Abstract This is the follow-up work of the ICFP 2019 paper “A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference”. We...