Verified Pauli-Product Measurement Compilation for Fault-Tolerant Quantum Computation
Dit artikel introduceert QPPM, een door Lean gemachiniseerd taal- en compositioneel verificatiekader voor fouttolerante kwantumcompilers dat weakest-precondition semantiek gebruikt om de correctheid van Pauli-product meetprogramma's te waarborgen, wat gecertificeerde circuitoptimalisatie mogelijk maakt die de logische meetdiepte vermindert terwijl de integriteit van de uitkomst behouden blijft en synthesefouten worden begrensd.