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

Lightweight Complex Matrices    (Matrix)

• Top
• Matrix Definitions and Equivalence
• Basic Matrices and Operations
  • Compatibility lemmas
• Matrix Properties
• Matrix Automation

The Building Blocks of Quantum Computing    (Qubit)

• Top
• Qubits
• Unitaries
  • Solving equations with square roots
• Measurement

Entanglement and Measurement    (Multiqubit)

• Top
• Multiple qubits and entanglement
• Total and partial measurement
  • Total measurement
  • Partial measurement

Quantum Programming in Coq    (SQIMP)

• Top
• A Small Quantum Imperative Language
  • Unitaries as gates
  • Denotation of Commands
  • Relating Quantum Programs
  • Superdense coding