About me

I am a researcher in the USTC-Yale Joint Research Center on High-Confidence Software of Computer Science Department, USTC.

Research on System Software Certification

I'm working on the certification of concurrent operating system kernels. Most modern kernels are preemptive, concurrent and lead to complex semantics. For verifying OS kernels, I try to define a formal certification framework, where correctness of kernels can be proved by foundational logic.

Theoretical Interests

I'm fond of many aspects of logic and lambda calculi, for example,


My most favorite programming language is CiC (Calculus of inductive Constructions). It is elegant and capable of expressing both computer programs and mathematical proofs. In Barendregt's lambda cube, CiC is the opposite vertex to the vertex as simple typed lambda calculus. CiC is the basic theory of the proof assistant Coq, which is a really good tool for studying logic and mathematical theory.


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

Quick Links