Dr. Zhong Shao

Biography

Zhong Shao is a Professor of Computer Science at Yale University. He earned his Ph.D. in Computer Science from Princeton University in 1994. His early career involved being a key developer and author of key compilation phases used in the Standard ML New Jersey compiler, where he built a type-based intermediate representation for a functional-language compiler. He designed and developed a production-quality type-preserving compiler for the Standard ML 1997 language and was the main architect of the FLINT certifying infrastructure. In recent years, his research has focused on developing and applying new language-based technologies to build certified system software, such as operating system kernels and hypervisors. His work in certified software involves creating binary machine executables that come with rigorous, machine-checkable proofs, ensuring the software is bug-free and meets specific requirements. Dr. Shao's current research addresses vital questions pertaining to the clean-slate approach, the right structures for OS kernels, and the development of programming languages and environments that facilitate the implementation of certified kernels, as well as new formal methods that support the development of languages that make certified kernels practical and scalable.

Research Interests