Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-11-20T07:32:26.841Z Has data issue: false hasContentIssue false

Types and typechecking for Communicating Quantum Processes

Published online by Cambridge University Press:  04 July 2006

SIMON J. GAY
Affiliation:
Department of Computing Science, University of Glasgow, U.K. Email: simon@dcs.gla.ac.uk
RAJAGOPAL NAGARAJAN
Affiliation:
Department of Computer Science, University of Warwick, U.K. Email: biju@dcs.warwick.ac.uk

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.

Type
Paper
Copyright
2006 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)