Shanghai Jiao Tong University
Bachelor of Engineering
2019.09 - Current
Major in Electrical EngineeringMinor in Computer Science
education
skills
Programming Language
CoqHaskellOCamlPascalPythonC/C++
Projects
Metaprogramming theory based on functional program
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.
PUBLICATIONS
CIRD-F: Spread and Influence of COVID-19 in China
(Co) First Auther
Journal of Shanghai Jiaotong University (Science) 25 (2), 147-156
- Auther: Lingyun Zhou* , Kaiwei Wu* , Hanzhi Liu* , 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
- Chi:
- Chi is a subset of Common Lisp, implemented in Python. Yet another mal, but with a funny lexer.
- STLC:
- 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.
- Strawberry Identification:
- 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.