I am currently a PhD student at McGill University, under the supervision of Professor Brigitte Pientka. I did my Master of Mathematics at the University of Waterloo, supervised by Professor Ondřej Lhoták. Before that, I worked in the industry since 2014. My undergrad was at Fudan University.

These days, I am mainly working on programming languages and formal proofs using proof assistants based on Martin-Löf type theory, e.g. Coq and Agda. I am particularly interested in various type theories and the mathematics behind them. As a purist, I insist that if a proof can be done constructively, then it needs to be; if a mechanized proof can be established, there is no reason not to.

Before heading back to school, I worked as an engineer on a number of projects involving performance engineering, configurations, and others that you might expect to see in the industry. Back in my old days at Fudan University, I was more of a robotic guy.

I am awarded the Postgraduate Scholarship-Doctoral by the Natural Sciences and Engineering Research Council of Canada.

I am in support of 996.icu activity .

Doctor of Philosophy

Computer Science

Grade: 4.0/4.0

09 / 2019 - present

Master of Mathematics

Computer Science

Grade: 94.4/100

Thesis: Decidability and Algorithmic Analysis of Dependent Object Types (DOT) (code) (slides)

Investigation on (un)decidability and algorithmic properties of the family of DOT calculi

Abstract

Dependent Object Types, or DOT, is a family of calculi developed to study the Scala programming language. These calculi have path dependent types as a feature, and potentially intersection types, union types and recursive types. So far, the study of DOT calculi mostly focuses on the soundness proof, which does not directly contribute to development of compilers. This thesis presents a detailed investigation of decidability and algorithmic properties of the family of DOT calculi.

In decidability analysis, the undecidability of subtyping of several calculi is formally established, including the D<: and D∧ calculi. Prior to this investigation, the undecidability of subtyping of all DOT calculi including D<: was open. Decidability analysis puts emphasis on a particular form of subtyping rules, called normal form. It turns out that a normal form definition is not only as expressive, but also more suggestive than the original definition. A conceptual device, called small-step analysis, is introduced to assist converting a usual definition of subtyping to its normal form definition. Moreover, decidability analysis gives direct contributions to the algorithmic analysis, by revealing two decidable fragments of D<: in declarative form, called the kernels. Decidability analysis also suggests a novel subtyping algorithm framework, stare-at subtyping. Stare-at subtyping and an existing algorithm are shown to be sound and complete w.r.t. their corresponding kernels.

In algorithmic analysis, stare-at subtyping is extended to other calculi, with more features than D<:, including D∧, μDART and jDOT. In μDART and jDOT, bi-directional type assignment algorithms are developed. The algorithms developed in this thesis are all shown to be sound with respect to their target calculi and terminating.

During the development of the algorithms, analysis shows a number of ways in which the Wadlerfest DOT calculus does not directly correspond to the Scala language, while substantially increases the difficulties of algorithmic design. jDOT, therefore, is developed as an alternative formalization of Scala.

09 / 2017 - 08 / 2019

Bachelor of Science

Electronic Engineering

Grade: 3.35/4.0

09 / 2010 - 07 / 2014

2021

Jason Hu and Ondřej Lhoták

2020

Teaching Assistant

COMP 360, Algorithm Design

COMP 302, Programming Languages and Paradigms

COMP 527, Logic and Computation

09 / 2019 - present

Teaching Assistant / Instructional Apprendice

CS 241, Foundation of Sequentual Programs

CS 343, Concurrent and Parallel Programming

09 / 2017 - 08 / 2019

summer 2021

2021

summer 2020

01/19/2020-01/25/2020

with fellowship

2019

2018

Applied Scientist Intern

05 / 2020 - 08 / 2020

Summer Analyst Intern

05 / 2018 - 08 / 2018

Java / Scala Developer

10 / 2015 - 07 / 2017

Software Developer

08 / 2014 - 10 / 2015

.Net Engineer Intern

05 / 2014 - 06 / 2014

QA Intern

07 / 2013 - 08 / 2013

09 / 2020 - 08 / 2023

09 / 2020 - 08 / 2024

09 / 2020 - 08 / 2021

01 / 2020 - 04 / 2020

I speak four languages: English, Mandarin, Cantonese and Japanese.

I am actively learning French at McGill now!

I had 6 years of math, 2 years of physics and 1 year of chemistry olympiads experience.

I am a Cantonese. My town is Foshan. Warning: I've got no idea how to perform Wing Chun.

I like superheroes, Marvel, DC and whatever you can name.

I played a lot of badminton during my undergrad, and now I resume to play again in Badminton Montreal!

I have lots of video games in my Steam library, and I dream to have time to play!