47 citations · 66 across the 7 of their papers we have counts for
7 papers
A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
Barış Bayazıt, Yao Li, Xujie Si
Large language models (LLMs) can potentially help with verification using proof assistants by automating proofs. However, it is unclear how effective LLMs are in this task. In this…
Freer Arrows and Why You Need Them in Haskell
Grant VanDomelen, Gan Shen, Lindsey Kuper +1
Freer monads are a useful structure commonly used in various domains due to their expressiveness. However, a known issue with freer monads is that they are not amenable to static a…
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 +4
Lazy evaluation is a powerful tool that enables better compositionality and potentially better performance in functional programming, but it is challenging to analyze its computati…
Program Adverbs and Tlön Embeddings
Yao Li, Stephanie Weirich
Free monads (and their variants) have become a popular general-purpose tool for representing the semantics of effectful programs in proof assistants. These data structures support…
Reasoning about the garden of forking paths
Yao Li, Li-yao Xia, Stephanie Weirich
Lazy evaluation is a powerful tool for functional programmers. It enables the concise expression of on-demand computation and a form of compositionality not available under other e…
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li +6
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie toge…
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code
Joachim Breitner, Antal Spector-Zabusky, Yao Li +3
Good tools can bring mechanical verification to programs written in mainstream functional languages. We use hs-to-coq to translate significant portions of Haskell's containers libr…