Quantum Information Logic

Origin. Coecke and others (2000s). Logic for quantum information flow. Entanglement and measurement. Categorical quantum mechanics. Types for quantum protocols.

Models. Qubits, entanglement, measurement. No-cloning, no-deleting. Teleportation protocol. Information-theoretic primitives. Type systems for quantum.

Formalism.

Quantum data types: qubit: 2-dimensional Hilbert space qubit ⊗ qubit: entangled pairs possible bit: classical measurement outcome

No-cloning theorem: ¬∃U. U|ψ⟩|0⟩ = |ψ⟩|ψ⟩ for all |ψ⟩ Cannot copy unknown quantum state.

Quantum teleportation: Alice has |ψ⟩ to send. Shared EPR pair |Φ⁺⟩ = (|00⟩ + |11⟩)/√2. Alice measures, sends 2 classical bits. Bob applies correction, gets |ψ⟩.

Types for quantum: Linear types enforce no-cloning. |ψ⟩: qubit cannot be duplicated. Classical bits can be copied.

Entanglement types: Bell states: maximally entangled. Separable: no entanglement. Type system can track entanglement.

Measurement: measure: qubit → bit Destroys superposition. ⟨0|ψ⟩|² + ⟨1|ψ⟩|² = 1

Quantum protocols: BB84 (key distribution). Superdense coding. Quantum error correction.

Symbols.

Symbol	Unicode	Name	Meaning
\|ψ⟩	—	Ket	Quantum state
⊗	U+2297	Tensor	Composite system
⟨ψ\|φ⟩	—	Inner product	Amplitude
U	—	Unitary	Quantum gate
M	—	Measure	Measurement

Metatheory. Soundness: protocols correct. No-go theorems as type errors. Categorical semantics in dagger categories. Completeness for fragments.

Applies to. Quantum protocol design. Verification. Cryptography. Error correction. Quantum software.

Limitations. Abstraction from physics details. Noise models limited. Scalability. Integration with full QM.