Yao Li, Assistant Professor at Portland State University

Yao Li (李垚), Ph.D.

Tenure-track Assistant Professor
Portland State University

About Me

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.

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

  • SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation

    by Sina Bagheri Nezhad, Yao Li, Ameeta Agrawal
    Findings of the Association for Computational Linguistics: EACL 2026
    Pre-print

  • The Memorist Tale: Every Thunk Every Cost All At Once

    by Xing Li, Yao Li, Peter Schachte, Christine Rizkallah
    35th European Symposium on Programming, ESOP 2026
    Pre-print Artifact

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

    by Barış Bayazıt, Yao Li, Xujie Si
    1st International Workshop on Language Models and Programming Languages, LMPL 2025
    Talk Paper OA Artifact

  • Freer Arrows and Why You Need Them in Haskell

    by Grant VanDomelen, Gan Shen, Lindsey Kuper, Yao Li
    18th ACM SIGPLAN International Symposium on Haskell, Haskell 2025
    Talk Paper OA Artifact

  • 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
    Talk Paper OA Artifact

  • Program Adverbs and Tlön Embeddings

    by Yao Li, Stephanie Weirich
    Proceedings of the ACM on Programming Languages, 6(ICFP), 2022 Distinguished Paper
    Talk Paper OA 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 OA 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 OA 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 OA Artifact
View All Publications

Talks

2024
  • Reasoning about Laziness is Reasoning about Future: Alternative Semantics to Lazy Evaluation
    Harvard PL Seminar, virtual talk
2023
  • "Shallower" Embeddings for Mechanized Reasoning
    PurPL (Purdue Programming Languages Group) Seminar, West Lafayette, IN
2022
  • 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
2021
  • 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
2020
  • Embracing a Mechanized Formalization Gap: Interactive reasoning for Haskell at scale
    Haskell Implementors' Workshop (HIW), co-located with ICFP, virtual talk
2018
  • The Science of Deep Specification
    NSF Expeditions in Computing - 10 Years of Transforming Science and Society, Washington, DC
2017
  • 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

  • ICFP Distinguished Paper Award, 2022
  • 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 SJTU, 2012
  • 1st Prize in 4th Intel Cup National Collegiate Software Innovation Contest, 2011

Hobbies

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