Liyi Li

31 papers A 4B 1C 2Journal 18Unranked 5
YearRankTypeTitle / Venue / Authors
2026 — conf
Validating Quantum State Preparation Programs.
ESOP (1)
Liyi Li, Anshu Sharma, Zoukarneini Difaizi Tagba, Sean Frett, Alex Potanin
2025 J jnl
A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware.
Proc. ACM Program. Lang.
Liyi Li, David Young, James Bryan Graves, Chandeepa Dissanayake, Amr Sabry
2025 J jnl
A Verified Compiler for Quantum Simulation.
CoRR
Liyi Li, Fenfen An, Federico Zahariev, Zhi Xiang Chong, Amr Sabry, Mark S. Gordon
2025 — conf
Differential Testing for Sequential to Parallel Transformations.
SC Workshops
Jobayer Ahmmed, Quazi Ishtiaque Mahmud, Junhyung Shim, Liyi Li, Ali Jannesari, Myra B. Cohen
2025 J jnl
Embedding Quantum Program Verification into Dafny.
Proc. ACM Program. Lang.
Feifei Cheng, Sushen Vangeepuram, Henry Allard, Seyed Mohammad Reza Jafari, Alex Potanin, Liyi Li
2025 J jnl
Quantum Simulation Programming via Typing.
CoRR
Liyi Li, Federico Zahariev, Chandeepa Dissanayake, Jae Swanepoel, Amr Sabry, Mark S. Gordon
2025 A conf
TypeFlexer: Type Directed Flexible Program Partitioning.
RAID
Arunkumar Bhattar, Liyi Li, Mingwei Zhu, Le Chang, Aravind Machiry
2025 J jnl
Validate Quantum State Preparation Programs.
CoRR
Liyi Li, Anshu Sharma, Zoukarneini Difaizi Tagba, Sean Frett, Alex Potanin
2024 J jnl
DisQ: A Markov Decision Process Based Language for Quantum Distributed Systems.
CoRR
Le Chang, Saitej Yavvari, Rance Cleaveland, Samik Basu, Liyi Li
2024 J jnl
Qafny: A Quantum-Program Verifier (Artifact).
Dagstuhl Artifacts Ser.
Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, Xiaodi Wu
2024 A conf
Qafny: A Quantum-Program Verifier.
ECOOP
Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, Xiaodi Wu
2024 J jnl
The Quantum Abstract Machine.
CoRR
Liyi Li, Le Chang, Rance Cleaveland, Mingwei Zhu, Xiaodi Wu
2023 J jnl
A Verified Optimizer for Quantum Circuits.
ACM Trans. Program. Lang. Syst.
Kesha Hietala, Robert Rand, Liyi Li, Shih-Han Hung, Xiaodi Wu, Michael Hicks
2023 J jnl
A formal model of Checked C.
J. Comput. Secur.
Liyi Li, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks
2023 J jnl
CheckedCBox: Type Directed Program Partitioning with Checked C for Incremental Spatial Memory Safety.
CoRR
Liyi Li, Arunkumar Bhattar, Le Chang, Mingwei Zhu, Aravind Machiry
2023 J jnl
Qunity: A Unified Language for Quantum and Classical Computing.
Proc. ACM Program. Lang.
Finn Voichick, Liyi Li, Robert Rand, Michael Hicks
2022 A conf
A Formal Model of Checked C.
CSF
Liyi Li, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks
2022 J jnl
A Formal Model of Checked C.
CoRR
Liyi Li, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks
2022 J jnl
A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm.
CoRR
Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks, Xiaodi Wu
2022 J jnl
Quantum Natural Proof: A New Perspective of Hybrid Quantum-Classical Program Verification.
CoRR
Liyi Li, Mingwei Zhu, Yi Lee, Le Chang, Xiaodi Wu
2022 J jnl
Verified compilation of Quantum oracles.
Proc. ACM Program. Lang.
Liyi Li, Finn Voichick, Kesha Hietala, Yuxiang Peng, Xiaodi Wu, Michael Hicks
2021 C conf
A Complete Semantics of $\mathbb {K}$ and Its Translation to Isabelle.
ICTAC
Liyi Li, Elsa L. Gunter
2021 B conf
Proving Quantum Programs Correct.
ITP
Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks
2021 J jnl
Verified Compilation of Quantum Oracles.
CoRR
Liyi Li, Finn Voichick, Kesha Hietala, Yuxiang Peng, Xiaodi Wu, Michael Hicks
2020 — —
A verification framework suitable for proving large language translations
Liyi Li
2020 A conf
K-LLVM: A Relatively Complete Semantics of LLVM IR.
ECOOP
Liyi Li, Elsa L. Gunter
2020 — conf
Per-Location Simulation.
NFM
Liyi Li, Elsa L. Gunter
2020 J jnl
Proving Quantum Programs Correct.
CoRR
Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks
2018 — conf
IsaK-Static: A Complete Static Semantics of \mathbb K.
FACS
Liyi Li, Elsa L. Gunter
2017 — conf
A Method to Translate Order-Sorted Algebras to Many-Sorted Algebras.
WPTE@FSCD
Liyi Li, Elsa L. Gunter
2014 C conf
Symbolic Analysis Tools for CSP.
ICTAC
Liyi Li, Elsa L. Gunter, William Mansky