I am currently a quantitative developer at Standard Chartered.
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.
PhD in Computer Science, 2018
The University of Hong Kong
BSc in Computer Science & Technology, 2014
Research middleware compiler from System F-based languages to Java with the Imperative Functional Object encoding