I will soon start my PhD at McGill University in September 2019!
I am currently a grad student at University of Waterloo, under the supervision of 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 writing up my Master's thesis, titled Decidability and Algorithmic Analysis of DOT.
I am in support of 996.icu activity .
CS 241, Foundation of Sequentual Programs
CS 343, Concurrent and Parallel Programming
I like superheroes, Marvel, DC and whatever you can name.
I used to play badminton during undergrad at Fudan with friends, but it turns out that it's hard to even find a reasonable court and shop for maintenance in Canada!
I have lots of video games in my Steam library, and I dream to have time to play!