Shanghai Jiao Tong University
Bachelor of Engineering
UndergraduateMajor in Electrical EngineeringMinor in Computer ScienceGPA: 3.72/4.3 Rank: 8/118 (first 2 year)
education
skills
Programming Language
CoqHaskellOCamlRustPascalPythonC/C++
Projects
Meta Programming Theories in Functional Languages
Research Project
2020.08 - 2021.02
Determine behaviors of object programs based on meta-programs.
- Learn Software foundations Volume 1&2 (Coq & operational semantics).
- Use Coq to formalize the semantics of the lambda calculus with constructors (meta-language).
- Build denotational semantics between meta-language and Coq.
- Prove the relationship between meta-programs and object programs.
- Download: Report\ Slides
Verification-aided Compiler Optimization
Research Project
2021.04 - Now
An expedition to support compiler optimization aided by verification information carried by programs.
PUBLICATIONS
CIRD-F: Spread and Influence of COVID-19 in China
(Co) First Author
Journal of Shanghai Jiaotong University (Science) 25 (2), 147-156
- Auther: Lingyun Zhou* , Hanzhi Liu* , Kaiwei Wu* , Yuanning Gao & Xiaofeng Gao
- Download:
AWARDS
The Interdisciplinary Contest in Modeling (ICM)
Meritorious Winner
2020
Zeyuan Scholarship of Shanghai Jiaotong University
Excellent Scholarship for Undergraduates of SJTU
B Class
OTHERS
Research Interests
Programming Language TheoryFormal Verification
Volunteer Service
Shanghai Marathon 2020POPL 2021 (Student Volunteer)
Toy Projects
OPG_Parser
Parser
- OPG (Operator Precedence Grammar) Parser, in Coq.
- Article:在Coq中实现算符优先文法分析器
- Github:MisakaCenter/OPG_Parser
RayTracer.ml
Computer Graphics
- Path tracer implemented in OCaml based on “Ray Tracing in One Weekend”.
- Implemented in OCaml.
- Github:MisakaCenter/RayTracer.ml
Pistolet
Programming Language
- Toy ML-like Imperative Programming Language.
- Implemented in Rust.
- Github:MisakaCenter/Pistolet
STLC
Programming Language
- Implement a simply typed lambda calculus read-eval-print-loop(REPL) in Coq & Haskell.
- Formalize the syntax and semantics of STLC in Coq.
- Transpile Coq Code to Haskell Code.
- Implement a REPL of STLC in Haskell.
- Github:MisakaCenter/STLC
Chi
Programming Language
- Chi is a subset of Common Lisp, implemented in Python. Yet another mal, but with a funny lexer.
- Github:MisakaCenter/Chi
Strawberry Identification
Machine Learning
- Implement strawberry identification function.
- Take a thousand photos of strawberries in the field, use LabelMe for data annotation, build a strawberry dataset.
- Use U-net for training, verify the accuracy, and get the strawberry identification model.
- Local:Strawberry Identification.pdf