Resource Estimation of Quantum Programs through Type Inference: QuRA and Shor’s Algorithm

Quantum computing promises to solve certain complex problems by exploiting the principles of quantum mechanics, such as superposition, which allows qubits to leverage parallelism in a way that differs from what is available in classical computing. Despite this potential, today’s quantum devices have significant limitations, such as high error rates, short coherence times, and a limited number of qubits. Accurately estimating the resources required by quantum algorithms — in particular, the number of qubits and operations — is essential to determine their feasibility on current and near-future hardware. This thesis addresses these challenges with QuRA, a tool for analysing the resource consumption of quantum programs. The approach is demonstrated through a detailed analysis of Shor’s algorithm, a key quantum algorithm with important implications for cryptography thanks to its ability to efficiently factor large integers, threatening to break protocols such as RSA. By providing mathematically supported guarantees on resource bounds, this work clarifies the practical requirements for implementing Shor’s algorithm. These contributions have significant implications both for the theoretical study and the practical realization of quantum computing.