Jason Hu

a.k.a. Zhong Sheng Hu

I have joined Amazon Web Services as an applied scientist in November 2024!
I almost(!, defence-only) obtain my PhD from 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 996.icu.


Education

McGill University

Montreal, QC

Doctor of Philosophy
Computer Science

Grade: 4.0/4.0

Thesis: Foundations and Applications of Modal Type Theories (code)

A series of studies of modal type theories in different styles, with applications in meta-programming

Abstract

Over the past few decades, type theories as mathematical foundations have been extensively studied and are well understood. Many proof assistants implement type theories and have found important applications to provide critical security guarantees. In these applications, users often write meta-programs, programs that generate other programs, to implement proof search heuristics and improve their work efficiency. However, as opposed to the deep understanding of type theories, it remains unclear what foundation is suitable to support meta-programming in proof assistants. In this thesis, I investigate modal type theories, a specific approach to this problem. In modal type theories, modalities are a way to shallowly embed syntax into the systems, so users can write meta-programs that manipulate syntax through these modalities.
I explore two different styles of modal systems. In the first part, I investigate the Kripke-style systems, which faithfully model the familiar quasi-quoting style of meta-programming. I develop an explicit substitution calculus and scale it to dependent types, introducing Mint. I prove strong normalization of Mint, which implies its logical consistency, using an untyped domain model.
Nevertheless, the Kripke-style systems only support composition and execution of code, and they cannot easily support a general recursion principle on the structure of code. To support such a general recursion principle, I develop the layered style, where a system is divided into nested layers of sub-languages. The layered style scales quite naturally to dependent types, introducing DeLaM. DeLaM allows users to compose, execute and recurse on dependently typed code. I prove that DeLaM is weakly normalizing and its convertibility problem between types and terms is decidable. Hence, DeLaM provides a type-theoretic foundation to support type-safe meta-programming in proof assistants.

Courses:
  • COMP 550 Natural Language Processing (report)
  • COMP 520 Compiler Design (report) (code)
  • COMP 596 Topics in Computer Science 3 (Theoretical Foundations of Reliable Meta-programming) (report)
  • COMP 700 Comprehensive Examination (report)
  • IFT 6172 Semantics of programming languages (at University of Montreal) (report) (code)
  • COMP 701 Thesis Proposal and Area Examination (report) (slides)
09 / 2019 - present

University of Waterloo

Waterloo, ON

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.

Courses:
  • CS 341 Algorithms
  • CS 745 Computer-Aided Verification
  • CS 766 Theory of Quantum Information (report)
  • ECE 653 Software Testing, Quality Assurance and Maintenance
  • CS 860 Advanced Topics in Algorithms and Complexity (report)
09 / 2017 - 08 / 2019

Fudan University

Shanghai, China

Bachelor of Science
Electronic Engineering

Grade: 3.35/4.0

09 / 2010 - 07 / 2014



Teaching

McGill University

Montreal, QC

Teaching Assistant

COMP 360, Algorithm Design
COMP 302, Programming Languages and Paradigms
COMP 527, Logic and Computation
COMP 523, Language-based Security

09 / 2019 - present

University of Waterloo

Waterloo, ON

Teaching Assistant / Instructional Apprendice

CS 241, Foundation of Sequentual Programs
CS 343, Concurrent and Parallel Programming

09 / 2017 - 08 / 2019

Activities

POPL 2023

artifact evaluation committee member

fall 2022

ICFP 2021

artifact evaluation committee member

summer 2021

HoTT Spring School (EPIT)

student

2021

ICFP 2020

artifact evaluation committee member

summer 2020

POPL 2020

student volunteer

01/19/2020-01/25/2020

Oregon Programming Languages Summer School

student

with fellowship

2019

DeepSpec Summer School

student

with fellowship

2018

Industry

Amazon Web Services

Seattle, WA

Applied Scientist II
11 / 2024 - present

Amazon Web Services

Minneapolis, MN

Applied Scientist Intern
05 / 2023 - 08 / 2023

Amazon Web Services

Boston, MA

Applied Scientist Intern
06 / 2022 - 09 / 2022

Amazon Web Services

Montreal, QC

Applied Scientist Intern
05 / 2020 - 08 / 2020

Morgan Stanley Services Canada Corp.

Montreal, QC

Summer Analyst Intern
05 / 2018 - 08 / 2018

Morgan Stanley Services Canada Corp.

Montreal, QC

Java / Scala Developer
10 / 2015 - 07 / 2017

Nexsan Technologies

Dorval, QC

Software Developer
08 / 2014 - 10 / 2015

Gridsum Technologies

Shanghai, China

.Net Engineer Intern
05 / 2014 - 06 / 2014

Virtuos

Shanghai, China

QA Intern
07 / 2013 - 08 / 2013

Scholarships

Postgraduate Scholarships-Doctoral

Natural Sciences and Engineering Research Council (NSERC)

09 / 2020 - 08 / 2023

Doctoral (B2X) Research Scholarship

Fonds de recherche du Québec - Nature et technologies (FRQNT)

09 / 2020 - 08 / 2024

Trottier Accelerator Award

School of Computer Science, McGill University

09 / 2020 - 08 / 2022

the Charity Exercise Award

School of Computer Science, McGill University

01 / 2020 - 04 / 2020

Other Info

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!