I am currently a quantitative developer at Standard Chartered.

I got my PhD in Computer Science from HKU PL Group advised by Dr. Bruno C. d. S. Oliveira. My research fields were programming languages, type systems and formal verification.

During my PhD studies, I worked on a JVM implementation of System F with support for full tail-call elimination (see this paper for more). I worked on the design of a dependently-typed calculus featuring general recursion and decidable type-checking (see this paper for more). I also worked on the design of a gradual type system with support for implicit higher-rank polymorphism – think of it as the first step towards Haskell-like languages with gradual typing (see this paper and also the journal version).

My PhD thesis is about the design of a type system featuring disjoint quantification and disjoint intersection types, which has great potential to serve as a foundation for powerful, flexible and yet type-safe and easy to reason object-oriented languages. See this paper and that for the theoretical foundation, and that for the first design of typed first-class traits.