Type-Based Verification of Connectivity Constraints in Lattice Surgery
<|reference_start|>Type-Based Verification of Connectivity Constraints in Lattice Surgery: 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.<|reference_end|>
@article{wakizaka2024type-based,
    title={Type-Based Verification of Connectivity Constraints in Lattice Surgery},
    author={Ryo Wakizaka, Yasunari Suzuki, Atsushi Igarashi},
    journal={arXiv preprint arXiv:2409.00529},
    year={2024},
    archivePrefix={arXiv},
    eprint={2409.00529},
    primaryClass={quant-ph cs.PL}
}