Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs
Este artículo presenta una lógica ligera de tipo Hoare derivada de la representación de Heisenberg de Gottesman para verificar eficientemente propiedades de circuitos de Clifford y la extiende a la computación cuántica universal mediante la incorporación de puertas y estados mágicos, permitiendo aplicaciones tales como la certificación de la eliminación de qubits, comprobaciones de separabilidad y el establecimiento de límites inferiores en la complejidad de las puertas .