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