Intuitionistic Unitary Linear Logic: A Proof-Theoretical Approach to Purely Quantum Higher-Order
Although the circuit model for quantum computation is well established, it is incapable of representing non-causal higher-order quantum processes such as the quantum switch. If several models of non-causal quantum computation have been considered in the literature, the approaches have so far only been focusing on the physicality of such processes, using matrices and other techniques from linear algebra. If these approaches are expressive, they however only provide a static and monolithic understanding of these processes. In this article, we propose a new formalism for non-causal, higher-order quantum processes. Based on a Curry-Howard interpetation, our proposal offers a computational interpretation that is both compositional and modular. In particular, we present Intuitionistic Unitary Linear Logic (IULL), a logic based on linear logic focusing on conservation of unitarity for higher order terms. We prove the coherence of IULLL, its completeness with regard to unitaries, and the admissibility of its cut rules. We finally discuss the validity of our approach by revisiting known non-causal quantum processes with IULL.