Dr. Zhong Shao

Biography

Zhong Shao is a Professor of Computer Science at Yale University. His research interests include programming languages, compilers, formal methods, and operating systems. He earned his Ph.D. in Computer Science from Princeton University in 1994. During his early career, he was a key developer and author of key compilation phases used in the Standard ML New Jersey compiler, building a type-based intermediate representation for the functional-language compiler. He designed and developed a production-quality type-preserving compiler for the entire Standard ML language and extended higher-order modules, becoming the main architect of the FLINT certifying infrastructure. In recent years, his interests have shifted towards developing and applying new language-based technologies to build certified system software, such as operating system kernels and hypervisors. Certified software consists of binary machine executable with rigorous machine-checkable proofs that ensure it is free of bugs and meets specific requirements. His work involves creating certified OS kernel libraries with formal specifications and proofs, examining abstraction layers in system libraries, and addressing important questions regarding the right OS kernel structures to support resilience, extensibility, and security. Additionally, he is developing programming languages and environments to implement certified kernels and exploring new formal methods to support new languages and make certified kernels practical and scalable.

Research Interests