About Me 👋
I am currently a Master's student in Embedded Systems at KTH Royal Institute of Technology (Stockholm). I am now conducting my Master's thesis at Institute of Science and Technology Austria (ISTA), under the supervision of Prof. Michael Sammler.
Previously, I received my Bachelor's degree in Electronic and Information Engineering from Huazhong University of Science and Technology (HUST), where I was a member of the Mathematics and Physics Honors Class.
My research interests span multiple areas in Programming Languages and Formal Verification, including dependent type theory (Lean4), separation logic (Iris), recursive subtyping, program calculation, and low-level code verification. Outside of research, I really enjoy watching football matches ⚽ and movies 🎬.
News 🔥
- [Feb 2026] Started Master's Thesis at ISTA Austria 🇦🇹, supervised by Michael Sammler.
- [Sep 2025] Joined EPFL LARA 🇨🇭 as an exchange student for semester project.
- [Jun 2025] Conducted Summer internship at KU Leuven 🇧🇪, supervised by Tom Schrijvers.
- [Jun 2025] Graduated from HUST with Honors Degree. 🎓
Education 🎓
M.Sc. in Embedded Systems
Exchange Student in Computer Science
B.Eng. in Electronic & Info. Engineering (Honor Class)
Research Experience 🔬
- Working on the foundational formalization and implementation of the Iris higher-order separation logic framework within the Lean4 ecosystem.
- Investigating modular reasoning techniques for concurrent programs by leveraging Lean4's advanced metaprogramming and type system capabilities.
- Implemented a rigorous shallow embedding of the Dependent Type Theory within the LISA proof assistant, strictly grounded in Zermelo-Fraenkel (ZF) set theory.
- Extended the set theory library with Grothendieck Universes (via Tarski's Axiom) to model predicative hierarchies and verified their closure properties.
- Developed a bidirectional Typecheck tactic that automatically synthesizes valid ZF proof objects for complex dependent type derivations (e.g., polymorphic Church encodings).
- Derived the QuickerSub algorithm from Weakly Positive Subtyping rules by applying Fold Fusion and Recursion Schemes (Zygomorphisms) to transform naive specifications into correct-by-construction implementations
- Optimized the iso-recursive subtyping check to O(nlogn) by employing advanced data structures (Lazy Sets and Cayley representations) for efficient variable binding management