Quantum Hoare Logic in Lean 4 is a quantum program verification tool. Implements quantum Hoare logic with classical variables to create formal, rigiourous proofs of the correctness of quantum programs.
-
Notifications
You must be signed in to change notification settings - Fork 1
Quantum Hoare Logic Lean 4 - A quantum program verification tool
License
alexjgreig/QHL-Lean
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
Quantum Hoare Logic Lean 4 - A quantum program verification tool
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published