## About me

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

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

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.

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

- Intuitionistic Logic
- Intuitionistic Type Theory
- Proof Theory
- Typed Lambda Calculus
- Computation Theory and Computability Theory
- Programming Languages Semantics

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