Publications

All 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

Pre-print Artifact Abstract
SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation

Sina Bagheri Nezhad, Yao Li, Ameeta Agrawal

Findings of the Association for Computational Linguistics: EACL 2026

Paper Pre-print Abstract
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

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

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

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

Paper Talk Artifact Abstract
Mechanized Reasoning about "how" Using Functional Programs and Embeddings

Yao Li

Ph.D. Dissertation, University of Pennsylvania Open Access

Paper Abstract
Program Adverbs and Tlön Embeddings

Yao Li, Stephanie Weirich

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

Paper Talk Artifact Abstract
Reasoning about the Garden of Forking Paths

Yao Li, Li-yao Xia, Stephanie Weirich

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

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

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

Paper Talk Artifact Abstract
Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language

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

Software Verification - 12th International Conference, VSTTE 2020

Paper Pre-print Artifact Abstract
A Scala based Framework for Developing Acceleration Systems with FPGAs

Yanqiang Liu, Yao Li, Zhengwei Qi, Haibing Guan

Journal of Systems Architecture, 98, 2019

Paper Abstract
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

The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 Open Access

Paper Abstract
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

Proceedings of the ACM on Programming Languages, 2(ICFP), 2018 Open Access

Paper Talk Artifact Abstract
Scala Based FPGA Design Flow (Abstract Only)

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

The 2017 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays, FPGA 2017

Paper Abstract
AutoBench: Finding Workloads That You Need Using Pluggable Hybrid Analyses

Yudi Zheng, Andrea Rosa, Luca Salucci, Yao Li, Haiyang Sun, Omar Javed, Lubomír Bulej, Lydia Y. Chen, Zhengwei Qi, Walter Binder

23rd IEEE International Conference on Software Analysis, Evolution, and Reengineering, SANER 2016

Paper Abstract
ScalaHDL: Express and Test Hardware Designs in a Scala DSL

Yao Li, Antonio R. Lopes, Zhouyun Xu, Zhengwei Qi, Haibing Guan

32nd IEEE International Conference on Computer Design, ICCD 2014

Paper Abstract

Drafts

Embracing a Mechanized Formalization Gap

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

Draft

Pre-print Talk Abstract