Experience

 
 
 
 
 

Quantitative Developer

Standard Chartered

Mar 2019 – Present Hong Kong
 
 
 
 
 

Part-time Research Assistant

The University of Hong Kong

Sep 2018 – Nov 2018 Hong Kong

Projects

FCore

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

Fi+

Coq formalization and implementation of the Fi+ calculus

SEDEL

Haskell implementation of a type system for first-class traits

GPC

Haskell implementation of Gradually Polymorphic Calculus

NeColus

Coq formalization of a coherent calculus with records and disjoint intersection types that supports nested composition

Talks

Calculi with disjoint intersection types support an introduction form for intersections called the merge operator, while retaining a …

Many dynamically typed languages (including JavaScript, Ruby, Python or Racket) support first-class classes, or related concepts such …

Consistent subtyping is employed in some gradual type systems to validate type conversions. The original definition by Siek and Taha …