Volume Q: Verified Quantum Computing
Table of Contents
Index
Roadmap
Rocq's Axiomatic Real Numbers (
Real
)
Axiomatizing the set R
The Field Equations
The Ring and Field tactics
Ordering
Completeness
Defining irrational numbers
Complex Numbers in Rocq (
Complex
)
Basic Definitions
Interlude: Psatz
C is a field
The complex conjugate
Sums over Complex Numbers
Solving equations with square roots
Lightweight Complex Matrices (
Matrix
)
Matrix Definitions and Equivalence
Basic Matrices and Operations
Compatibility lemmas
Matrix Properties
Matrix Automation
Matrix Library
The Building Blocks of Quantum Computing (
Qubit
)
Qubits
Unitaries
Measurement
Entanglement and Measurement (
Multiqubit
)
Multiple qubits and entanglement
Total and partial measurement
Total measurement
Partial measurement
Automation
Quantum Programming in Rocq (
SQIR
)
A Small Quantum Intermediate Representation
Unitaries as gates
Denotation of Commands
New Gates and Proofs
Rewriting Circuits
Circuit Families
Superdense coding
Quantum Teleportation
Deutsch's Algorithm
