Yu-Fang Chen, Philipp Rümmer, Wei-Lun Tsai: A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification). CADE 2023: 170-189