Current Projects

• DeepSpec Web Server, building a formally verified HTTP server on a formally verified operating system.  Link
• Haskell to Coq, mechanically verifying Haskell programs using Coq proof assistant.  Link

Publications

• Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code (Experience Report)
  by Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Stephanie Weirich
  the ACM SIGPLAN International Conference on Functional Programming (ICFP), 2018
   Paper  Extended Version
• AutoBench: Finding Workloads That You Need Using Pluggable Hybrid Analyses
  by Yudi Zheng, Andrea Rosa, Luca Salucci, Yao Li, Haiyang Sun, Lubomir Bulej, Lydia Y. Chen, Zhengwei Qi, and Walter Binder
  23rd IEEE International Conference on Software Analysis, Evolution, and Reengineering (SANER), 2016
   Paper
• ScalaHDL: Express and Test Hardware Designs in a Scala DSL
  by Yao Li, Antonio R. Lopes, Zhouyun Xu, Zhengwei Qi, and Haibing Guan,
  32nd IEEE International Conference on Computer Design (ICCD), 2014
   Paper

Teaching

• Teaching Assistant: Theory of Computation (University of Pensylvania), 2018 Spring
• Teaching Assistant: Advanced Programming (University of Pennsylvania), 2017 Fall
• Teaching Assistant: Programming and Data Structures II (Shanghai Jiao Tong University), 2013 Fall

Honors & Awards

• Google Open Source Peer Bonus (for Scala Forklift), 2018
• Outstanding Graduate of Shanghai Jiao Tong University, 2016
• China National Scholarship (the scholarship with highest honor and reward), 2014
• Outstanding Graduate of Shanghai Jiao Tong University, 2013
• China National Scholarship (the scholarship with highest honor and reward), 2012
• Most Popular Collegiate Innovation Projects of Shanghai Jiao Tong University, 2012
• 1st Prize in the 4th Intel Cup National Collegiate Software Innovation Contest in China, 2011
• 1st Prize in National Olympiad in Informatics in Provinces, 2008
• 1st Prize in National Olympiad in Informatics in Provinces, 2007