Research Interests

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.

Current Ph.D. Students

• Laura Israel
• Ian Kariniemi
• Yiming Lin
• Grant VanDomelen
• Nicholas Coltharp

(I'm currently at capacity, so I do not take new Ph.D. students.)

Teaching

• CS 410/510 TOP: Proof Assistants and Program Verification, Spring, 2025
• CS 358: Principles of Programming Languages, Spring, 2025
• CS 457/557: Functional Programming, Fall, 2024
• CS 410/510 TOP: Advanced Topics in Program Verification, Spring, 2024
• CS 457/557: Functional Programming, Winter, 2024
• CS 410/510 TOP: Proof Assistants and Program Verification, Spring, 2023
• CS 457/557: Functional Programming, Winter, 2023

Featured Publications

• Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs
  by Li-yao Xia, Laura Israel, Maite Kramarz, Nicholas Coltharp, Koen Claessen, Stephanie Weirich, Yao Li
  Proceedings of the ACM on Programming Languages, 8(ICFP), 2024
   Paper (Open Access)  Pre-print  Artifact
• 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...

Talks

• Reasoning about Laziness is Reasoning about Future: Alternative Semantics to Lazy Evaluation
  Harvard PL Seminar, virtual talk, 2024
• "Shallower" Embeddings for Mechanized Reasoning
  PurPL (Purdue Programming Languages Group) Seminar, West Lafayette, IN, 2023
• 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

Services

• Program Committee: TyDe'25, POPL'25, CoqPL'25, PLDI'24, TFP'24, POPL'24 SRC, PLDI'23, PLDI'23 SRC
• External Reviewer: OOPSLA'25, JFP, CONCUR'23, ESOP'23, ECOOP'23, WoLLIC'23
• Organizing Committee: PLDI'25 (Publicity Co-Chair), PLDI'24 (Publicity Co-Chair), SPLASH'22 (Student Volunteer Co-Chair)
• Artifact Evaluation Committee: ECOOP'23, POPL'22, ICFP'21, POPL'21
• Session Chair: PLDI'23, SPLASH'21
• Mentor: DeepSpec REU'21 (UPenn), Google Summer of Code (Scala) 2016
• Student Volunteer: CIS Doctoral Association at Penn (Spring 2021), ICFP'21, ICFP'20, DeepSpec Summer School'17

Honors & Awards

• 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

Hobbies

• Puzzles, escape rooms, board games, tabletop RPGs (Pathfinder 2e, D&D 5e)
• Still learning: Leung Sheung Wing Chun, archery