photo

MisakaCenter

Hanzhi Liu
Shanghai, China

education

Shanghai Jiao Tong University

Bachelor of Engineering

Undergraduate
2019.09 - Now

Major in Electrical EngineeringMinor in Computer ScienceGPA: 3.72/4.3 Rank: 8/118 (first 2 year)

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: Hanzhi Liu* , Lingyun Zhou* , Kaiwei Wu* , Yuanning Gao & Xiaofeng Gao
  • Download:

The Dynamic Persuasive and Informative Advertising Strategy of a Two-part Tariff Monopolist with Advertising Spillover Effects

Second Author

In preparation
  • Auther: Lingyun Zhou, Hanzhi Liu and Genyuan Zhong
  • Submitted to Journal of the Operational Research Society

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

RayTracer.ml

Computer Graphics

2021.07
  • Path tracer implemented in OCaml based on “Ray Tracing in One Weekend”.
  • Implemented in OCaml.
  • Github:MisakaCenter/RayTracer.ml

Pistolet

Programming Language

2021.03

STLC

Programming Language

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

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

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