Yao Li (李垚), Ph.D.

Student researchers and alumni in my group.

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

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

   Nicholas Coltharp, Steven Libby, Laura Israel, Yao Li

   FLOPS 2026

   Paper Pre-print Artifact

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

   Xing Li, Yao Li, Peter Schachte, Christine Rizkallah

   ESOP 2026

   Paper Artifact

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

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

6. Freer Arrows and Why You Need Them in Haskell

   Grant VanDomelen, Gan Shen, Lindsey Kuper, Yao Li

   Haskell 2025 Open Access

   Paper Talk Artifact

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

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

   Yao Li

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

   Paper

9. Program adverbs and Tlön embeddings

   Yao Li, Stephanie Weirich

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

   Paper Talk Artifact

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

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

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

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

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

    Yanqiang Liu, Yao Li, Zhengwei Qi, Haibing Guan

    J. Syst. Archit., 98 2019

    Paper

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

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

17. Scala Based FPGA Design Flow (Abstract Only)

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

    FPGA 2017

    Paper

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

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

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

    ICCD 2014

    Paper

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

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

3. Embracing a mechanized formalization gap

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

   Draft 2019

   Pre-print Talk

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

   Portland PL Symposium (PorPL)

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