Linear and Non-linear Relational Analyses for Quantum Program Optimization

Watch a 21-minute conference talk from POPL 2025 where researchers Matthew Amy and Joseph Lunderville from Simon Fraser University present their work on extending quantum program optimization techniques. Learn how phase folding optimization can be re-formulated as an affine relation analysis, enabling its application to quantum programs with complex classical control flow including nested loops and procedure calls. Discover how classical relational domains, particularly non-linear relations, can enhance optimization capabilities for circuits involving classical arithmetic. The presentation explains how the sum-over-paths technique extracts precise symbolic transition relations from straightline circuits, allowing the inference of non-linear relations even from gate sets with only linear operations like Clifford+t. Experimental results demonstrate the generation of non-trivial loop invariants for quantum program optimization and achievements in optimizing common circuits that previously required manual intervention. The talk includes references to available artifacts that have been evaluated as reusable.