Biography
Hi, this is Tony, a junior Computer Science student in Shanghai Jiao Tong University.
Coding is fun / What’s past is prologue
My research interest includes Programming Language, Functional Programming and Formal Verification. I am actively looking for a PL PhD position in 2022 fall.
Download my resumé.
Interests
- Formal Verification
- Programming Languages
- Functional Programming
Education
-
Non-Graduating Exchange Student, 2021 Fall
National University of Singapore (School of Computing)
-
BSc in Computer Science (IEEE Pilot Class), 2018-2022(Expected)
Shanghai Jiao Tong University
Experience
Software Engineer Intern
In Visual and Parallel Computing Group, developed a web-based automation tool to smooth the testing workflow of graphics drivers.
Research Intern
Participate in following projects in Programming Languages.
- Used OCaml to implement some instances of interpreters, compilers and virtual machine models of lambda calculus.
- Using Teyjus, a high-order logic programming language, to implement various functional language compilation phases (e.g., lambda lifting, uncurrying, lambda shrinking).
- Prove the correctness(semantic preservation) of the above compilation transformations using logical relations in Abella (Still ongoing)
Research Intern
Participate in following projects in Formal Verification using Coq.
- Verify the correctness of the theory of real number construction.
- Reason about the functional correctness of several classical graph algorithms (e.g., Tarjan’s algorithm for Strongly-Connected-Components) and their C implementations in VST.
- Build and prove the soundness of a control-flow splitting tool based on VST to simplify verification proof of assertion-annotated C programs.
Projects
*
