My first research project was on verification-aided optimization. My colleagues and I implemented a deep-embedded version of VST, VST-A [1], and part of VST-Floyd in Coq. Then, we were able to use verified program annotation to guide the optimization pass, ensuring its soundness. In this project, I mainly worked on verified symbolic execution, which serves as a solid foundation of program correctness. This work will be covered in my bachelor's thesis.

My second project was an optimizing zero-knowledge circuit compiler. Zero-knowledge circuits are a relatively new computation model, and we were trying to fill the gap in optimizing compilers for it. I evaluated manual optimizations done by domain experts and designed an optimization-friendly FRP-style IR. We defined a cost-minimizing synthesizing problem on top of that then. I'm no longer actively working on this project, so please consult the authors for up-to-date information.

[1]: https://arxiv.org/pdf/1909.00097.pdf, accepted to POPL'24