I am a tenure-track assistant professor at Portland State University.
I obtained my Ph.D. in computer and information science from the University of Pennsylvania in 2022, under the guidance of Stephanie Weirich.
You can call me Yao. My preferred pronoun is he/him or they/them.

My research aims to (1) advance the state of the art of verification on real-world software and (2) make verification easier to use from a programming languages perspective.

I am looking for students! Please send me an email if you are interested in programming languages/formal verification/interactive theorem proving.

  • Program Adverbs and Tlön Embeddings
    by Yao Li, Stephanie Weirich
    Proceedings of the ACM on Programming Languages, 6(ICFP), 2022 (Distinguished Paper)
     Paper (Open Access)  Pre-print  Artifact
  • Reasoning about the Garden of Forking Paths
    by Yao Li, Li-yao Xia, Stephanie Weirich
    Proceedings of the ACM on Programming Languages, 5(ICFP), 2021
     Talk  Paper (Open Access)  Pre-print  Artifact
  • Verifying an HTTP Key-Value Server with Interaction Trees and VST
    by Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, Steve Zdancewic
    12th International Conference on Interactive Theorem Proving, ITP 2021
     Paper (Open Access)  Artifact
  • Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code
    by Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua Cohen, Stephanie Weirich
    Journal of Functional Programming, 31(e5), 2021
     Talk  Paper (Open Access)  Artifact
  • 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, Steve Zdancewic
    The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019
     Paper (Open Access)  Pre-print
  • More...
  • The Expression Problem and Theorem Proving (Discussion)
    Workshop on the Implementation of Type Systems (WITS), co-located with POPL, Philadelphia, PA, 2022
  • Effect-Oblivious Equivalence
    Workshop on Principles of Secure Compilation (PriSC), co-located with POPL, Philadelphia, PA, 2022
  • Reasoning about the Garden of Forking Paths
    POPV seminar at Boston University (Longer Version, Invited Talk), 2021
    The ACM SIGPLAN International Conference on Functional Programming (ICFP), virtual talk, 2021
    The ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH), Chicago, IL, 2021
  • Embracing a Mechanized Formalization Gap: Interactive reasoning for Haskell at scale
    Haskell Implementors’ Workshop (HIW), co-located with ICFP, virtual talk, 2020
  • The Science of Deep Specification
    NSF Expeditions in Computing - 10 Years of Transforming Science and Society, Washington, DC, 2018
  • Dependent Types in Scala
    Philly Area Scala Enthusiasts Meetup (PHASE), Philadelphia, PA, 2017
  • Scala-Forklift: Type-Safe Data Migration Tool for Slick, Git and Beyond
    Comcast Scala By the Schuyllkill Conference, Philadelphia, PA, 2017
  • Program Committee: PLDI'23
  • External Reviewer: ECOOP'23
  • Student Volunteer Co-Chair: SPLASH'22
  • Artifact Evaluation Committee: ECOOP'23, POPL'22, ICFP'21, POPL'21
  • Session Chair: SPLASH'21
  • Mentor: DeepSpec REU'21 (UPenn), Google Summer of Code (Scala) 2016
  • Student Volunteer: ICFP'21, ICFP'20, DeepSpec Summer School'17
  • Google Open Source Peer Bonus (for Scala Forklift), 2018
  • Outstanding Graduate of Shanghai Jiao Tong University, 2016
  • China National Scholarship, 2014
  • Outstanding Graduate of Shanghai Jiao Tong University, 2013
  • China National Scholarship, 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
  • Puzzles, escape rooms, board games
  • Still learning: fencing, archery