Siyuan He


hesy@umich.edu

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.

Resume he662 at purdue dot edu Github Linkedin (outdated)

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

Ph.D.

2021 -

Master

2019 - 2021

Bachelor

2016 - 2020

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