A logical analysis of entanglement and separability in quantum higher-order functions

TL;DR

This paper introduces a novel logical framework for analyzing entanglement and separability in a functional quantum programming language, addressing the complexities introduced by higher-order functions and quantum non-determinism.

Contribution

It is the first to propose a logical analysis specifically for entanglement and separability in a higher-order functional quantum language.

Findings

Developed a non-compositional logical analysis for quantum entanglement.

Addressed challenges posed by quantum non-determinism in logical assertions.

Pioneered a formal method for entanglement analysis in functional quantum programming.

Abstract

We present a logical separability analysis for a functional quantum computation language. This logic is inspired by previous works on logical analysis of aliasing for imperative functional programs. Both analyses share similarities notably because they are highly non-compositional. Quantum setting is harder to deal with since it introduces non determinism and thus considerably modifies semantics and validity of logical assertions. This logic is the first proposal of entanglement/separability analysis dealing with a functional quantum programming language with higher-order functions.