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

  • Mechanized Reasoning about "how" Using Functional Programs and Embeddings
    by Yao Li
    Ph.D. Dissertation, University of Pennsylvania
     Paper (Open Access)  Abstract

  • Program Adverbs and Tlön Embeddings
    by Yao Li, Stephanie Weirich
    Proceedings of the ACM on Programming Languages, 6(ICFP), 2022 (Distinguished Paper)
     Paper (Open Access)  Pre-print  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 (Open Access)  Pre-print  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 (Open Access)  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 (Open Access)  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 (Open Access)  Pre-print  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 (Open Access)  Pre-print  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

  • Embracing a Mechanized Formalization Gap
    by Antal Spector-Zabusky, Joachim Breitner, Yao Li, Stephanie Weirich
     Talk  Pre-print  Abstract