On Multiplicative Linear Logic, Modality and Quantum Circuits

TL;DR

This paper introduces QMLL, a logical system based on linear logic with a quantum modality, capable of representing and computing all unitary quantum circuits through a concrete GoI interpretation.

Contribution

It presents QMLL, a novel logical framework that captures all unitary quantum circuits and provides a proof-theoretic foundation for quantum computation.

Findings

QMLL can represent all unitary quantum circuits.

Proofs in QMLL correspond to quantum circuits via GoI interpretation.

QMLL enjoys cut-elimination, ensuring consistency and normalization.

Abstract

A logical system derived from linear logic and called QMLL is introduced and shown able to capture all unitary quantum circuits. Conversely, any proof is shown to compute, through a concrete GoI interpretation, some quantum circuits. The system QMLL, which enjoys cut-elimination, is obtained by endowing multiplicative linear logic with a quantum modality.