Building Extensible Program Logics through Effect Handlers
Zichen Zhang, Simon Oddershede Gregersen, and Joseph Tassarotti. 2025. Building Extensible Program Logics through Effect Handlers. Under review. https://u8cat.github.io/files/ficus.pdf
CV
Education
- Ph.D. in Computer Science, New York University, Sep 2024—
- B.E. in Computer Science & Technology, University of Science and Technology of China, Sep 2020—Jun 2024
- High School, Shenzhen Middle School, Sep 2017—Jul 2020
Work experience
- Summer & Fall 2023: Research Assistant
- University of Michigan
- Duties included: Conducting research on SQL verification
- Supervisor: Prof. Xinyu Wang
Skills
- Computer Languages:
- Proof Assistants: Rocq, Lean
- General Purpose Languages: Python, C++, Go, C, OCaml, Rust
- Hardware Description Languages: Verilog
- Assembly Languages: RISC-V, ARMv7, LoongArch, AMD64
- Other Languages: Antlr, LaTeX, LLVM, Yacc (Bison)
- Natural Languages: English (fluent), Mandarin (native)
Publications
Talks
Building Extensible Program Logics with Effect Handlers
Talk at Schwarzman College of Computing Building, MIT, Cambridge, Middlesex, MA, United States
A Coq Mechanized Formalization of Realistic SQL Query Optimization Rules
Talk at 六安曙光铂尊酒店, Jin'an, Lu'an, AH, China
TranGo: Transparent Hybrid Go Bindings Generation for C Libraries
Talk at 东区理化大楼东三报告厅, USTC, Baohe, Hefei, AH, China
TranGo: Transparent Hybrid Go Bindings Generation for C Libraries
Talk at 西区特种实验室报告厅, USTC, Shushan, Hefei, AH, China
Teaching
Service and leadership
- Student Volunteer in USTC CS Debugger Salon, Spring 2023 & Spring 2024
Misc
- My preferred timezone is Coordinated Universal Time (UTC).
- My preferred temperature unit is Kelvin (K).
- My name in native alphabet is 张子辰 (U+5F20 U+5B50 U+8FB0).