photo

MisakaCenter

Hanzhi Liu
misaka@sjtu.edu.cn
misaka.center
MisakaCenter
Shanghai, China

education

Shanghai Jiao Tong University

Bachelor of Engineering

Undergraduate
2019.09 - Current

Major in Electrical EngineeringMinor in Computer ScienceGPA: 89.24/100 Rank:1/119 (first year)

National University of Singapore

Workshop

NUS SOC 2021 Summer Workshop
2021.05 - 2021.08 (Expected)

Algorithm, Cloud & Security

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

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: Hanzhi Liu* , Lingyun Zhou* , 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

  • 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.