I'm a Ph.D. student in computer science at Purdue University in West Lafayette since Fall 2021, working under the instruction of professor Tiark Rompf.
My primary research interest is programming language, more specifically, type/effect systems and polymorphisms. I am also interested in formal verification, VST, and verifiable C.
My ongoing project involves a lightweight polymorphic type system and destructive effects over reachability.
305 N. University Street, West Lafayette, IN 47907 (Due to COVID, please contact online)
Other past interest areas: machine learning, computer vision, causal inference, network, OS.
Games: World of Warcraft, Age of Empire 2, Diablo 3/4, Honkai series, Counter-Strike, LoL, and so on.
Personals: Music (piano & guitar), Calligraphy, Poems & Proses, watching sea seals
Education
Teaching
Teaching Assistant at SJTU
VE370: Computer Organization
- 2019 Summer
Teaching Assistant at Purdue
CS354: Operating Systems
- 2022 Fall
- 2023 Spring
- 2023 Fall
CS352: Compilers
- 2024 Spring
Primary Research
Reachability Types
Lambda star type system, with reachability types, enables expressive ownership-style reasoning on higher-order functions. We use a qualifier (reachability set) that binded with normal types to track the alias that the term can observe from the environment. I.e., many features can be developed based on the lambda star system, i.e. flow-sensitive effect system, ownership transfer, polymorphisms.
Lambda star system is still under development, here is a list of things I'm involved in (with other members):
- Prototype effect system
- (to be announced later)
September 2021 -
Previous Research
Formal verification of a path-finding algorithm
University of Michigan, Advisor: Prof. Jean-Baptiste Jeannin
- Design a path-finding solution for airport taxiing problem under constrains of Air-Traffic-Control.
- Implement the solution and formalize the correctness.
- Verify the correctness of the path-finding algorithm and graph mapping algorithms in Coq.
November 2020 - August 2021
Hazel: Extraction to OCaml,
University of Michigan - Future of Programming Lab, Advisor: Prof. Cyrus Omar.
- Extraction from Hazel AST to OCaml code
December 2019 - 2021
Concurrent DeepWeb
University of Illinois at Chicago, Advisor: Prof. William Mansky.
- Concurrent verified web server, modifying based on DeepWeb. Pending due to iTree difficulty.
August 2020 - present (pending)
Publication
-
Verification of an Airport Taxiway Path-Finding Algorithm. Siyuan He, Ke Du, Joshua Wilhelm and Jean-Baptiste Jeannin. In Digital Aerospace Systems Conference (DASC 2020), to appear.
Assessing Humor in Edited News Headlines
SI630 Course Project & Online Competition
Build a NLP model to predict the level of humor of a editing operation that replace one word in a newspaper headline. The most innovative point is encoding the editing action into a vector representation, which is a new topic with almost no research or reference.
February 2020 - April 2020
Temperature Forecasting
Master Capstone Design
Propose a model to forecast the temperature of a certain place, which involves time series forecasting. Our model features deep learning based model and extra features, which beats some common models.
February 2021 - April 2021
Anomaly Detection in Injection Molding
Bachelor Capstone Design
Propose a model to detect anomaly in the injection molding process of industrial plastic production. The project is sponsored by Foxconn.
May 2020 - August 2020
MIPS CPU
SJTU VE370 Course Project
Use Verilog to implement a MIPS pipeline CPU to support basic instructions.
February 2019 - May 2019
Search engine on games
UM SI650 Course Project
Implemented a domain-specific search engine, featuring static ranking, filter on dislike, pseudo relevance feed-back, spell correction and query suggestion.
2019 Fall
Multivariate Cryptography
SJTU VE475 Course Project
Overview and implement the multivariate cryptography structure. Provide a simple proof for the NP-hardness of the MQ problem.
2019 Summer
Clustering based on potential and repulsion
SJTU VE488 Course Project || Further Research
Introduce the repulsion and potential in physics to clustering method. Develop and implement a fast clustering approximation method.
2018 Summer
Intern Experience
Computer Vision Researcher
Lenovo AI-Lab, Beijing
- Develop a blur detection method and optimize the pre-processing efficiency.
- Optimize the align performance and overall recall of the face recognition model.
December 2017 - February 2018
Data Analysis
Nokia Shanghai-Bell, Shanghai
- Involved in smart street-lamp network project, complete all lab tests and find problems.
- Involved in the design of frontend and backend of a smart education system.
- Develop an automation program to take over manual work in daily form filling.
May 2020 - August 2020