Supervisors

Suitable for

Abstract

Prerequisites: Recommended courses include 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. Currently, there is no mechanization of such calculi exists. A mechanized formalization will enable researchers to prove different protocols’ properties rigorously.

Focus

In this project, you will implement a quantum process calculus and its semantics in Coq Proof Assistant [4], a dependently typed interactive proof assistant.

Method

• Essential goal: A mechanized implementation of the process calculus and its semantics.

• 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/