Skip to main content
University of Oxford Department of Computer Science
  Contact Us     Search  
  1. Home
  2. Student Space
  3. Online Resources, Handbooks & Library
  4. Student projects - Consolidation in Quantum Concurrent Processes

Consolidation in Quantum Concurrent Processes

Supervisors

Nobuko Yoshida
Atalay Ileri

Suitable for

MSc in Advanced Computer Science
Mathematics and Computer Science, Part C
Computer Science and Philosophy, Part C
Computer Science, Part C

Abstract

Prerequisites:  Recommended courses include Distributed Processes, Types and Programming (for MSC), Lambda calculus and types, and (Quantum Information or Quantum Processes and Computation). Familiarity with functional programming, Coq, and dependent types would be advantageous.

 

Background

  • CQP and other process calculi [1, 2, 3] are presented to define quantum protocols among two or more participants that can run quantum operations and send and receive qubits. These calculi require each participant to have local access to a quantum computer to carry out the protocol. However, since quantum computers are prohibitively expensive and not commercially available, the mentioned requirement limits their applicability.

Focus

In this project, you will aid the design of an algorithm that consolidates all quantum operations in a single process while preserving the semantics of the protocol. In addition, you will implement a quantum process calculi, the transformation procedure, and prove the semantic preservation of the transformation in Coq Proof Assistant [4], a dependently typed interactive proof assistant.

Method

  • Essential goal: A protocol transformation algorithm with mechanized semantic preservation proofs.
  • Stretch-goals:
    • - Mechanized implementation of a process calculus and its semantics.
    • - Implementation of the transformation algorithm.
    • - Mechanized proofs of semantic preservation.

 

References

  • [1] Simon J. Gay and Rajagopal Nagarajan. 2006. Types and typechecking for Communicating Quantum Processes. Mathematical. Structures in Comp. Sci. 16, 3 (June 2006), 375–406. https://doi.org/10.1017/S0960129506005263
  • [2] Mingsheng Ying, Yuan Feng, Runyao Duan, and Zhengfeng Ji. 2009. An algebra of quantum processes. ACM Trans. Comput. Logic 10, 3, Article 19 (April 2009), 36 pages. https://doi.org/10.1145/1507244.1507249
  • [3] Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. 2024. Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic Observers. Proc. ACM Program. Lang. 8, POPL, Article 43 (January 2024), 29 pages. https://doi.org/10.1145/3632885
  • [4] https://coq.inria.fr/

Student Space

Back to Top