Yao Li (李垚), Ph.D.

Tenure-track Assistant Professor
Portland State University

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.

Yao Li, Assistant Professor at Portland State University

Research Group

Student researchers and alumni in my group.

Current Ph.D. Students

I am currently at capacity and not taking new Ph.D. students.

Past Students

Teaching

CS 669: Scholarship Skills

Winter, 2026

CS 457/557: Functional Programming

Fall, 2025

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

Unifying Hindsight and Foresight: Lazy Cost Analysis as Functional Logic Programming

Nicholas Coltharp, Steven Libby, Laura Israel, Yao Li

18th International Symposium on Functional and Logic Programming 2026
Pre-print Artifact

The Memorist Tale: Every Thunk Every Cost All At Once

Xing Li, Yao Li, Peter Schachte, Christine Rizkallah

35th European Symposium on Programming, ESOP 2026 2025
Pre-print Artifact

A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants

Barış Bayazıt, Yao Li, Xujie Si

1st International Workshop on Language Models and Programming Languages, LMPL 2025 2025 Open Access
Paper Talk Artifact

Freer Arrows and Why You Need Them in Haskell

Grant VanDomelen, Gan Shen, Lindsey Kuper, Yao Li

18th ACM SIGPLAN International Symposium on Haskell, Haskell 2025 2025 Open Access
Paper Talk Artifact

Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs

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 2024 Open Access
Paper Talk Artifact

Program Adverbs and Tlön Embeddings

Yao Li, Stephanie Weirich

Proceedings of the ACM on Programming Languages, 6(ICFP), 2022 2022 Open Access Distinguished Paper
Paper Talk Artifact

Reasoning about the Garden of Forking Paths

Yao Li, Li-yao Xia, Stephanie Weirich

Proceedings of the ACM on Programming Languages, 5(ICFP), 2021 2021 Open Access
Paper Talk Artifact

Verifying an HTTP Key-Value Server with Interaction Trees and VST

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 2021 Open Access
Paper Artifact

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code

Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua Cohen, Stephanie Weirich

Journal of Functional Programming, 31(e5), 2021 2021 Open Access
Paper Talk Artifact

View All Publications

Talks

  1. Reasoning about Laziness is Reasoning about Future: Alternative Semantics to Lazy Evaluation

    Harvard PL Seminar, virtual talk

  2. "Shallower" Embeddings for Mechanized Reasoning

    PurPL (Purdue Programming Languages Group) Seminar, West Lafayette, IN

  3. The Expression Problem and Theorem Proving (Discussion)

    Workshop on the Implementation of Type Systems (WITS), co-located with POPL, Philadelphia, PA

    Effect-Oblivious Equivalence

    Workshop on Principles of Secure Compilation (PriSC), co-located with POPL, Philadelphia, PA

  4. Reasoning about the Garden of Forking Paths

    • POPV seminar at Boston University (Longer Version, Invited Talk)
    • The ACM SIGPLAN International Conference on Functional Programming (ICFP), virtual talk
    • The ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH), Chicago, IL

  5. Embracing a Mechanized Formalization Gap: Interactive reasoning for Haskell at scale

    Haskell Implementors' Workshop (HIW), co-located with ICFP, virtual talk

  6. The Science of Deep Specification

    NSF Expeditions in Computing - 10 Years of Transforming Science and Society, Washington, DC

  7. Dependent Types in Scala

    Philly Area Scala Enthusiasts Meetup (PHASE), Philadelphia, PA

    Scala-Forklift: Type-Safe Data Migration Tool for Slick, Git and Beyond

    Comcast Scala By the Schuyllkill Conference, Philadelphia, PA

Service & Awards

Academic Service

Program Committee
TyDe'25 POPL'25 CoqPL'25 PLDI'24 TFP'24 POPL'24 SRC PLDI'23 PLDI'23 SRC
External Reviewer
Automated Software Engineering (Journal) CPP'26 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

Honors & Awards

  1. 2022 ICFP Distinguished Paper Award
  2. 2018 Google Open Source Peer Bonus (for Scala Forklift)
  3. 2016 Outstanding Graduate of Shanghai Jiao Tong University
  4. 2014 China National Scholarship
  5. 2013 Outstanding Graduate of Shanghai Jiao Tong University
  6. 2012 China National Scholarship
  7. 2012 Most Popular Collegiate Innovation Projects of SJTU
  8. 2011 1st Prize in 4th Intel Cup National Collegiate Software Innovation Contest

Hobbies

Puzzles Escape Rooms Tabletop RPGs (Pathfinder 2e, D&D 5e) Leung Sheung Wing Chun Archery