Validate Quantum State Preparation Programs.
CoRR, January, 2025
Qafny: A Quantum-Program Verifier (Artifact).
Dagstuhl Artifacts Ser., 2024
DisQ: A Markov Decision Process Based Language for Quantum Distributed Systems.
CoRR, 2024
The Quantum Abstract Machine.
CoRR, 2024
Qafny: A Quantum-Program Verifier.
Proceedings of the 38th European Conference on Object-Oriented Programming, 2024
A Verified Optimizer for Quantum Circuits.
ACM Trans. Program. Lang. Syst., September, 2023
Qunity: A Unified Language for Quantum and Classical Computing.
Proc. ACM Program. Lang., January, 2023
A formal model of Checked C.
J. Comput. Secur., 2023
CheckedCBox: Type Directed Program Partitioning with Checked C for Incremental Spatial Memory Safety.
CoRR, 2023
Verified compilation of Quantum oracles.
Proc. ACM Program. Lang., 2022
Quantum Natural Proof: A New Perspective of Hybrid Quantum-Classical Program Verification.
CoRR, 2022
A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm.
CoRR, 2022
Proving Quantum Programs Correct.
Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021
A Complete Semantics of $\mathbb {K}$ and Its Translation to Isabelle.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2021, 2021
A verification framework suitable for proving large language translations
PhD thesis, 2020
Proceedings of the NASA Formal Methods - 12th International Symposium, 2020
K-LLVM: A Relatively Complete Semantics of LLVM IR.
Proceedings of the 34th European Conference on Object-Oriented Programming, 2020
IsaK-Static: A Complete Static Semantics of \mathbb K.
Proceedings of the Formal Aspects of Component Software - 15th International Conference, 2018
A Method to Translate Order-Sorted Algebras to Many-Sorted Algebras.
Proceedings of the Proceedings Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation, 2017
Symbolic Analysis Tools for CSP.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2014, 2014