The Library
Types and typechecking for communicating quantum processes
Tools
Tools
Tools
Gay, Simon J. and Nagarajan, Rajagopal. (2010) Types and typechecking for communicating quantum processes. Mathematical Structures in Computer Science, Vol.16 (No.3). pp. 375-406. ISSN 0960-1295
Full text not available from this repository.
Official URL: http://dx.doi.org/10.1017/S0960129506005263
Abstract
We define a language CQP (Communicating Quantum Processes) for modelling systems that combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and transformation of the quantum state; in particular, quantum bits (qubits) can be transmitted from process to process along communication channels. CQP has a static type system, which classifies channels, distinguishes between quantum and classical data, and controls the use of quantum states. We formally define the syntax, operational semantics and type system of CQP, prove that the semantics preserves typing, and prove that typing guarantees that each qubit is owned by a unique process within a system. We also define a typechecking algorithm and prove that it is sound and complete with respect to the type system. We illustrate CQP by defining models of several quantum communication systems, and outline our plans for using CQP as the foundation for formal analysis and verification of combined quantum and classical systems.
| Item Type: | Journal Article |
|---|---|
| Subjects: | Q Science > QA Mathematics > QA75 (Please use QA76 Electronic Computers. Computer Science) |
| Divisions: | Faculty of Science > Computer Science |
| Journal or Publication Title: | Mathematical Structures in Computer Science |
| Publisher: | Cambridge University Press |
| ISSN: | 0960-1295 |
| Date: | June 2010 |
| Volume: | Vol.16 |
| Number: | No.3 |
| Page Range: | pp. 375-406 |
| Identification Number: | 10.1017/S0960129506005263 |
| Status: | Peer Reviewed |
| Publication Status: | Published |
| Access rights to Published version: | Restricted or Subscription Access |
| Funder: | Engineering and Physical Sciences Research Council (EPSRC), EU Sixth Framework Programme (FP6) |
| Grant number: | GR/S34090 (EPSRC), Project SecoQC (FP6) |
| Related URLs: | |
| URI: | http://wrap.warwick.ac.uk/id/eprint/46186 |
Actions (login required)
 |
View Item |
