Type-Based Verification of Connectivity Constraints in Lattice Surgery

Abstract

Fault-tolerant quantum computation using lattice surgery can be abstracted as operations on graphs, wherein each logical qubit corresponds to a vertex of the graph, and multi-qubit measurements are accomplished by connecting the vertices with paths between them. Operations attempting to connect vertices without a valid path will result in abnormal termination. As the permissible paths may evolve during execution, it is necessary to statically verify that the execution of a quantum program can be completed. This paper introduces a type-based method to statically verify that well-typed programs can be executed without encountering halts induced by surgery operations. Alongside, we present ${\mathcal{Q}}_{LS}$, a first-order quantum programming language to formalize the execution model of surgery operations. Furthermore, we provide a type checking algorithm by reducing the type checking problem to the offline dynamic connectivity problem.

29 pages, the extended version of the paper accepted by APLAS 2024

References in corpus (21)

• Fault-tolerant quantum computation by anyons
• Surface codes: Towards practical large-scale quantum computation
• Universal Quantum Computation with ideal Clifford gates and noisy ancillas
• Suppressing quantum errors by scaling a surface code logical qubit
• Logical quantum processor based on reconfigurable atom arrays
• Topological Quantum Distillation
• How to factor 2048 bit RSA integers in 8 hours using 20 million noisy qubits
• Surface code quantum computing by lattice surgery
• A Game of Surface Codes: Large-Scale Quantum Computing with Lattice Surgery
• Encoding Electronic Spectra in Quantum Circuits with Linear T Complexity
• Even more efficient quantum computations of chemistry through tensor hypercontraction
• Entangling logical qubits with lattice surgery
• Towards Large-scale Functional Verification of Universal Quantum Circuits
• PyZX: Large Scale Automated Diagrammatic Reasoning
• A Verified Optimizer for Quantum Circuits
• Universal quantum computing with twist-free and temporally encoded lattice surgery
• Assessing requirements to scale to practical quantum advantage
• Surface code compilation via edge-disjoint paths
• Equivalence Checking of Quantum Circuits with the ZX-Calculus
• Demonstration of logical qubits and repeated error correction with better-than-physical error rates
• Optimising Clifford Circuits with Quantomatic