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
Paper
(Open Access)
Pre-print Abstract Artifact
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
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
Drafts
Embracing a Mechanized Formalization Gap
by Antal Spector-Zabusky, Joachim Breitner, Yao Li, Stephanie Weirich Talk Pre-print Abstract