Zhuang, Zhong(庄重)'s Home Page

I am a Ph.D candidate in the USTC-Yale Joint Research Center on High-Confidence Software of Computer Science Department, USTC. My advisor is Prof. Yiyun Chen.

I'm working on certifying compiler and automated theorem provers. Modern certifying compilers always generate lots of proof obligations, I'm trying to ease the process of certifying programs.

• Compiler
• Program verification
• Theorem Prover
• Coq and other proof assistants
• Type Theory

• Tactic for Separation Logic

  Draft Paper,Download

A Certifying Compiler for Clike Subset of C Language. Zhaopeng Li, Zhong Zhuang, Yiyun Chen, Simin Yang, Zhenting Zhang and Dawei Fan. Accepted by the 4th IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'10), August 25 - 27, 2010, Taipei, Taiwan, China (pdf)

• Tactic in Coq
• Linux(Debian),GNU/Emacs
• C,Java,OCaml,Sml/NJ,Haskell,Ruby

Email: echo "dyzz {at} mail_ustc_edu_cn" |sed -e 's/_/\./g' -e 's/\s*{at}\s*/@/'