30 citations · 55 across the 6 of their papers we have counts for
4 papers · 1 filter
Qafny: A Quantum-Program Verifier
Liyi Li, Mingwei Zhu, Rance Cleaveland +4
Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specificati…
A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm
Yuxiang Peng, Kesha Hietala, Runzhou Tao +4
Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but these are only useful if computed answers are correct. While hardware-level…
Qunity: A Unified Language for Quantum and Classical Computing (Extended Version)
Finn Voichick, Liyi Li, Robert Rand +1
We introduce Qunity, a new quantum programming language designed to treat quantum computing as a natural generalization of classical computing. Qunity presents a unified syntax whe…
A Formal Model of Checked C
Liyi Li, Yiyun Liu, Deena L. Postol +3
We present a formal model of Checked C, a dialect of C that aims to enforce spatial memory safety. Our model pays particular attention to the semantics of dynamically sized, potent…