Reasoning about Entanglement and Separability in Quantum Higher-Order Functions