Yao Li (李垚), Ph.D.

Tenure-track Assistant Professor
Portland State University

I develop programming-language techniques for building reliable systems, analyzing the cost of lazy programs, and improving AI-assisted verification.

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

My research connects programming-language semantics with mechanized reasoning. These selected works illustrate three directions in this agenda.

Building and verifying reliable software systems

I develop programming abstractions for coordinating distributed programs and techniques for verifying existing software. This includes library-level choreographic programming, interaction-tree specifications, and proof-guided simplification.

  1. Freer Arrows and Why You Need Them in Haskell

    Freer arrows support static analysis of computations in Haskell, with choreographic programming as a case study.

    Haskell 2025 Open Access

    Paper Talk Artifact

  2. Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees

    Proof-guided local-variable lifting produces simplified interaction-tree programs and equivalence proofs together.

    ITP 2026

    Paper Pre-print Artifact

Mechanized cost analysis of lazy programs

I develop semantic models and mechanized proofs for the cost of lazy evaluation, including amortized analysis of persistent data structures.

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

    Bidirectional demand semantics supports mechanized cost analysis of lazy programs, including proofs about amortization and persistent data structures.

    Proc. ACM Program. Lang., 8(ICFP) 2024 Open Access

    Paper Talk Artifact

  2. The Memorist Tale: Every Thunk Every Cost All At Once

    Deterministic memorist semantics records fine-grained cost and usage information through a monadic interface.

    ESOP 2026

    Paper Artifact

AI-assisted verification and reliable generated code

I study how large language models can assist proof development, and how formal verification and executable checks can assess the reliability of generated code.

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

    A case study examines LLM proof generation in hs-to-coq and Verdi, including the effects of dependencies and source-file context.

    LMPL 2025 Open Access

    Paper Talk Artifact

Complete publications and draftsResearch groupTeaching

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 358: Principles of Programming Languages

Spring, 2026 · Spring, 2025

Learn how programming languages work, from syntax to semantics.

CS 669: Scholarship Skills

Winter, 2026

Practice research, writing, presenting, and reviewing in computer science.

Public course materials are not available on this page.

CS 457/557: Functional Programming

Fall, 2025 · Fall, 2024 · Winter, 2024 · Winter, 2023

Learn functional programming in Haskell to write clear, modular code.

CS 410/510 TOP: Proof Assistants and Program Verification

Spring, 2025 · Spring, 2023

Use Coq to build machine-checked proofs of program correctness.

CS 410/510 TOP: Advanced Topics in Program Verification

Spring, 2024

Explore classical and modern approaches to program verification.

Publications

2026

  1. Agent-Native Research Artifacts

    Jiachen Liu, Jiaxin Pei, Jintao Huang, Chenglei Si, Ao Qu, Xiangru Tang, Runyu Lu, Lichang Chen, Xiaoyan Bai, Haizhong Zheng, Carl Chen, Zhiyang Chen, Haojie Ye, Yujuan Fu, Zexue He, Zijian Jin, Zhenyu Zhang, Shangquan Sun, Maestro Harmon, John Dianzhuo Wang, Jianqiao Zeng, Jiachen Sun, Mingyuan Wu, Baoyu Zhou, Chenyu You, Shijian Lu, Yiming Qiu, Fan Lai, Yuan Yuan, Yao Li, Junyuan Hong, Ruihao Zhu, Beidi Chen, Alex Pentland, Ang Chen, Mosharaf Chowdhury, Zechen Zhang

    NeurIPS 2026

    Pre-print

  2. Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees

    Yiming Lin, Ian Kariniemi, Yao Li

    ITP 2026

    Paper Pre-print Artifact

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

    Nicholas Coltharp, Steven Libby, Laura Israel, Yao Li

    FLOPS 2026

    Paper Pre-print Talk Artifact

  4. The Memorist Tale: Every Thunk Every Cost All At Once

    Xing Li, Yao Li, Peter Schachte, Christine Rizkallah

    ESOP 2026

    Paper Artifact

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

    Sina Bagheri Nezhad, Yao Li, Ameeta Agrawal

    Findings of EACL 2026

    Paper Pre-print

2025

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

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

    LMPL 2025 Open Access

    Paper Talk Artifact

  2. Freer Arrows and Why You Need Them in Haskell

    Grant VanDomelen, Gan Shen, Lindsey Kuper, Yao Li

    Haskell 2025 Open Access

    Paper Talk Artifact

2024

  1. 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

    Proc. ACM Program. Lang., 8(ICFP) 2024 Open Access

    Paper Talk Artifact

2022

  1. Mechanized Reasoning about "how" Using Functional Programs and Embeddings

    Yao Li

    Ph.D. Dissertation, University of Pennsylvania 2022 Open Access

    Paper

  2. Program adverbs and Tlön embeddings

    Yao Li, Stephanie Weirich

    Proc. ACM Program. Lang., 6(ICFP) 2022 Open Access Distinguished Paper

    Paper Talk Artifact

2021

  1. Reasoning about the garden of forking paths

    Yao Li, Li-yao Xia, Stephanie Weirich

    Proc. ACM Program. Lang., 5(ICFP) 2021 Open Access

    Paper Talk Artifact

  2. 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 C. Pierce, Steve Zdancewic

    ITP 2021 Open Access

    Paper Artifact

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

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

    J. Funct. Program., 31 2021 Open Access

    Paper Talk Artifact

2020

  1. Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language

    Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel

    VSTTE 2020

    Paper Pre-print Artifact

2019

  1. A scala based framework for developing acceleration systems with FPGAs

    Yanqiang Liu, Yao Li, Zhengwei Qi, Haibing Guan

    J. Syst. Archit., 98 2019

    Paper

  2. From C to interaction trees: specifying, verifying, and testing a networked server

    Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic

    CPP 2019 Open Access

    Paper

2018

  1. Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report)

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

    Proc. ACM Program. Lang., 2(ICFP) 2018 Open Access

    Paper Talk Artifact

2017

  1. Scala Based FPGA Design Flow (Abstract Only)

    Yanqiang Liu, Yao Li, Weilun Xiong, Meng Lai, Cheng Chen, Zhengwei Qi, Haibing Guan

    FPGA 2017

    Paper

2016

  1. AutoBench: Finding Workloads That You Need Using Pluggable Hybrid Analyses

    Yudi Zheng, Andrea Rosà, Luca Salucci, Yao Li, Haiyang Sun, Omar Javed, Lubomı́r Bulej, Lydia Y. Chen, Zhengwei Qi, Walter Binder

    SANER 2016

    Paper

2014

  1. ScalaHDL: Express and test hardware designs in a Scala DSL

    Yao Li, Antonio Roldao Lopes, Zhouyun Xu, Zhengwei Qi, Haibing Guan

    ICCD 2014

    Paper

Drafts

2026

  1. A Taxonomy of Predicate Transformer Monads for Specifying Monadic Programs

    Abigail Pribisova, Yao Li, Cezar-Constantin Andrici, Catalin Hritcu, Kenji Maillard, Exequiel Rivas

    Draft 2026 Submitted to ESOP 2027

    Pre-print

  2. The Memorist Tale: Every Thunk Every Cost All At Once (Extended Version)

    Xing Li, Yao Li, Peter Schachte, Christine Rizkallah

    Draft 2026 Submitted to ACM TOPLAS (extended version of the ESOP 2026 paper)

  3. Parkour: Parallel Library-Level Choreographic Programming

    Gan Shen, Grant VanDomelen, Jonathan Castello, Yao Li, Lindsey Kuper

    Draft 2026 Submitted to ACM TOPLAS Special Issue on Multiparty Languages

    Pre-print

2019

  1. Embracing a mechanized formalization gap

    Antal Spector-Zabusky, Joachim Breitner, Yao Li, Stephanie Weirich

    Draft 2019

    Pre-print Talk

Talks

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

    Harvard PL Seminar, virtual talk

  3. "Shallower" Embeddings for Mechanized Reasoning

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

  4. 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

  5. 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

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

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

  7. The Science of Deep Specification

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

  8. 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
CPP'27 Haskell'26 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)
Founder & Organizer
PorPL
Member-At-Large
Haskell Symposium
Artifact Evaluation Committee
ECOOP'23 POPL'22 ICFP'21 POPL'21
Session Chair
Haskell'26 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