All Publications

  • 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 Abstract 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 Abstract 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 Abstract Artifact

  • Mechanized Reasoning about "how" Using Functional Programs and Embeddings

    by Yao Li
    Ph.D. Dissertation, University of Pennsylvania
    Paper OA Abstract

  • 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 Abstract 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 Abstract 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 Abstract 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 Abstract Artifact

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

    by Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel
    Software Verification - 12th International Conference, VSTTE 2020
    Paper Pre-print Abstract Artifact

  • A Scala based Framework for Developing Acceleration Systems with FPGAs

    by 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

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

  • Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code (Experience Report)

    by Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Stephanie Weirich
    Proceedings of the ACM on Programming Languages, 2(ICFP), 2018
    Talk Paper OA Abstract Artifact

  • Scala Based FPGA Design Flow (Abstract Only)

    by 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

    by 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

    by Yao Li, Antonio R. Lopes, Zhouyun Xu, Zhengwei Qi, Haibing Guan
    32nd IEEE International Conference on Computer Design, ICCD 2014
    Paper Abstract

Drafts

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

    by Sina Bagheri Nezhad, Yao Li, Ameeta Agrawal
    Pre-print Abstract

  • Embracing a Mechanized Formalization Gap

    by Antal Spector-Zabusky, Joachim Breitner, Yao Li, Stephanie Weirich
    Talk Pre-print Abstract