Skip to content Skip to navigation
University of Warwick
  • Study
  • |
  • Research
  • |
  • Business
  • |
  • Alumni
  • |
  • News
  • |
  • About

University of Warwick
Publications service & WRAP

Highlight your research

  • WRAP
    • Home
    • Search WRAP
    • Browse by Warwick Author
    • Browse WRAP by Year
    • Browse WRAP by Subject
    • Browse WRAP by Department
    • Browse WRAP by Funder
    • Browse Theses by Department
  • Publications Service
    • Home
    • Search Publications Service
    • Browse by Warwick Author
    • Browse Publications service by Year
    • Browse Publications service by Subject
    • Browse Publications service by Department
    • Browse Publications service by Funder
  • Help & Advice
University of Warwick

The Library

  • Login
  • Admin

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. doi:10.1017/S0960129506005263 ISSN 0960-1295.

Research output not available from this repository.

Request-a-Copy directly from author or use local Library Get it For Me service.

Official URL: http://dx.doi.org/10.1017/S0960129506005263

Request Changes to record.

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 > QA76 Electronic computers. Computer science. Computer software
Divisions: Faculty of Science, Engineering and Medicine > Science > Computer Science
Journal or Publication Title: Mathematical Structures in Computer Science
Publisher: Cambridge University Press
ISSN: 0960-1295
Official Date: June 2010
Dates:
DateEvent
June 2010Published
Volume: Vol.16
Number: No.3
Page Range: pp. 375-406
DOI: 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)

Request changes or add full text files to a record

Repository staff actions (login required)

View Item View Item
twitter

Email us: wrap@warwick.ac.uk
Contact Details
About Us