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