ScalaHDL: Express and test hardware designs in a Scala DSL. - Yao Li 004; Antonio Roldao Lopes; Zhouyun Xu; Zhengwei Qi; Haibing Guan (ICCD, 2014)

AutoBench: Finding Workloads That You Need Using Pluggable Hybrid Analyses. - Yudi Zheng; Andrea Rosà; Luca Salucci; Yao Li 004; Haiyang Sun 003; Omar Javed; Lubomír Bulej; Lydia Y. Chen; Zhengwei Qi; Walter Binder (SANER, 2016)

Scala Based FPGA Design Flow (Abstract Only). - Yanqiang Liu; Yao Li 004; Weilun Xiong; Meng Lai; Cheng Chen; Zhengwei Qi; Haibing Guan (FPGA, 2017)

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Stephanie Weirich (CoRR, 2018)

Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Stephanie Weirich (Proc. ACM Program. Lang., 2018)

From C to interaction trees: specifying, verifying, and testing a networked server. - Nicolas Koh; Yao Li 004; Yishuai Li; Li-yao Xia; Lennart Beringer; Wolf Honoré; William Mansky; Benjamin C. Pierce; Steve Zdancewic (CPP, 2019)

Embracing a mechanized formalization gap. - Antal Spector-Zabusky; Joachim Breitner; Yao Li 004; Stephanie Weirich (CoRR, 2019)

A scala based framework for developing acceleration systems with FPGAs. - Yanqiang Liu; Yao Li 004; Zhengwei Qi; Haibing Guan (J. Syst. Archit., 2019)

Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language. - Jay Bosamiya; Sydney Gibson; Yao Li 004; Bryan Parno; Chris Hawblitzel (VSTTE, 2020)

Verifying an HTTP Key-Value Server with Interaction Trees and VST. - Hengchu Zhang; Wolf Honoré; Nicolas Koh; Yao Li 004; Yishuai Li; Li-yao Xia; Lennart Beringer; William Mansky; Benjamin C. Pierce; Steve Zdancewic (ITP, 2021)

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Joshua M. Cohen; Stephanie Weirich (J. Funct. Program., 2021)

Reasoning about the garden of forking paths. - Yao Li 004; Li-yao Xia; Stephanie Weirich (Proc. ACM Program. Lang., 2021)

Program adverbs and Tlön embeddings. - Yao Li 004; Stephanie Weirich (Proc. ACM Program. Lang., 2022)

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 004 (Proc. ACM Program. Lang., 2024)