How to Sign Paper Contracts? Conjectures & Evidence Related to Equitable & Efficient Collaborative Task Scheduling. - Eric Brier; David Naccache; Li-yao Xia (IACR Cryptol. ePrint Arch., 2013)

How to Sign Paper Contracts? Conjectures and Evidence Related to Equitable and Efficient Collaborative Task Scheduling. - Eric Brier; David Naccache; Li-yao Xia (Open Problems in Mathematics and Computational Science, 2014)

Beginner's luck: a language for property-based generators. - Leonidas Lampropoulos; Diane Gallois-Wong; Catalin Hritcu; John Hughes 001; Benjamin C. Pierce; Li-yao Xia (POPL, 2017)

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)

Composing Bidirectional Programs Monadically. - Li-yao Xia; Dominic Orchard; Meng Wang 002 (ESOP, 2019)

Composing bidirectional programs monadically (with appendices). - Li-yao Xia; Dominic Orchard; Meng Wang 002 (CoRR, 2019)

Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress). - Li-yao Xia; Yannick Zakowski; Paul He; Chung-Kil Hur; Gregory Malecha; Benjamin C. Pierce; Steve Zdancewic (CoRR, 2019)

Luck: A Probabilistic Language for Testing. - Leonidas Lampropoulos; Benjamin C. Pierce; Li-yao Xia; Diane Gallois-Wong; Catalin Hritcu; John Hughes 001 (Foundations of Probabilistic Programming, 2020)

Interaction trees: representing recursive and impure programs in Coq. - Li-yao Xia; Yannick Zakowski; Paul He; Chung-Kil Hur; Gregory Malecha; Benjamin C. Pierce; Steve Zdancewic (Proc. ACM Program. Lang., 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)

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

C4: verified transactional objects. - Mohsen Lesani; Li-yao Xia; Anders Kaseorg; Christian J. Bell; Adam Chlipala; Benjamin C. Pierce; Steve Zdancewic (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)