All Publications

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

Drafts

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

    Draft 2026

    Pre-print

  4. Embracing a mechanized formalization gap

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

    Draft 2019

    Pre-print Talk