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

• From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
  by Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
  8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), 2019
   Paper  Pre-print
• 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
   Talk  Paper  Extended Version
• AutoBench: Finding Workloads That You Need Using Pluggable Hybrid Analyses
  by Yudi Zheng, Andrea Rosa, Luca Salucci, Yao Li, Haiyang Sun, Omar Javed, Lubomír 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

Experience

• Research Intern at Microsoft
  Jun. 2018 - Aug. 2018, Redmond, WA, USA
  Vale Project, under supervision of Chris Hawblitzel
• Visiting Researcher at University of Lugano
  Mar. 2015 - Jun. 2015, Lugano, Ticino, Switzerland
  Dynamic Analysis Group, under supervision of Walter Binder
• Software Development Engineer Intern at Microsoft
  Jun. 2012 - Sep. 2012, Shanghai, China
  Infrastructure team, under supervision of Zhiliang Xu

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