### Abstract

A formalization of the theory of quantum and classical registers as developed by (Unruh, Quantum and Classical Registers). In a nutshell, a register refers to a part of a larger memory or system that can be accessed independently. Registers can be constructed from other registers and several (compatible) registers can be composed. This formalization develops both the generic theory of registers as well as specific instantiations for classical and quantum registers.

### License

BSD License

### Topics

- Computer science/Algorithms/Quantum computing
- Computer science/Programming languages/Logics
- Computer science/Semantics and reasoning

### Session Registers

- Axioms
- Laws
- Axioms_Complement
- Laws_Complement
- Axioms_Classical
- Laws_Classical
- Misc
- Classical_Extra
- Finite_Tensor_Product
- Axioms_Quantum
- Laws_Quantum
- Quantum
- Quantum_Extra
- QHoare
- Finite_Tensor_Product_Matrices
- Teleport
- Axioms_Complement_Quantum
- Laws_Complement_Quantum
- Quantum_Extra2
- Pure_States
- Check_Autogenerated_Files

### Depends on

- Complex Bounded Operators

## Cite

×

Registers-AFP

    @article{Registers-AFP,
      author  = {Dominique Unruh},
      title   = {Quantum and Classical Registers},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Registers.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Nov 7, 2021 : Isabelle2021