Software Foundations Logo
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