Typed compositional quantum computation with lenses
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2023
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866917480068284416 |
|---|---|
| author | Garrigue, Jacques Saikawa, Takafumi |
| author_facet | Garrigue, Jacques Saikawa, Takafumi |
| contents | We propose a type-theoretic framework for describing and proving properties of quantum computations, in particular those presented as quantum circuits. Our proposal is based on an observation that, in the polymorphic type system of Coq, currying on quantum states allows us to apply quantum gates directly inside a complex circuit. By introducing a discrete notion of lens to control this currying, we are further able to separate the combinatorics of the circuit structure from the computational content of gates. We apply our development to define quantum circuits recursively from the bottom up, and prove their correctness compositionally. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2311_14347 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Typed compositional quantum computation with lenses Garrigue, Jacques Saikawa, Takafumi Programming Languages Logic in Computer Science We propose a type-theoretic framework for describing and proving properties of quantum computations, in particular those presented as quantum circuits. Our proposal is based on an observation that, in the polymorphic type system of Coq, currying on quantum states allows us to apply quantum gates directly inside a complex circuit. By introducing a discrete notion of lens to control this currying, we are further able to separate the combinatorics of the circuit structure from the computational content of gates. We apply our development to define quantum circuits recursively from the bottom up, and prove their correctness compositionally. |
| title | Typed compositional quantum computation with lenses |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2311.14347 |