Article index
Four volumes, eight starting points. Follow one idea to the next question.
Mathematical foundations
The mathematical language of quantum states, operations and circuits.
Quantum States and OperationsQuantum States and Operations
State vectors, density matrices, quantum operations, and measurement branches provide the mathematical basis for quantum programs.
Quantum CircuitsQuantum Circuits
Quantum circuits compose gates, measurements, and classical control to describe transformations and observable probabilities.
Quantum languages
How programs are expressed, and how types govern quantum resources.
Linear Type SystemsLinear Type Systems
Linear types track quantum resources explicitly while allowing ordinary classical data to be reused when the language permits it.
Quantum Programming LanguagesQuantum Programming Languages
Quantum languages combine quantum operations with classical computation, explicit resource management, and well-defined measurement behavior.
Program semantics
A mathematical account of syntax, execution and observable behavior.
Denotational SemanticsDenotational Semantics
Denotational semantics assigns compositional mathematical meanings to quantum commands, measurement branches, and potentially nonterminating computations.
Weakest PreconditionsWeakest Preconditions
Adjoint quantum operations transform postconditions backward, with distinct weakest and weakest liberal preconditions for total and partial correctness.
Logic & verification
Assertions, inference rules and mechanized proofs of correctness.
Quantum Hoare LogicQuantum Hoare Logic
Quantum Hoare logic uses operator-valued predicates to distinguish partial correctness from total correctness through precise trace inequalities.
Verification Methods and ToolsVerification Methods and Tools
Quantum verification combines precise specifications, symbolic reasoning, proof tools, and testing while making assumptions and trust boundaries explicit.