Non-harmonious logical connectives have recently been shown to provide a natural proof-theoretic account of quantum measurement. In particular, the connective \(\mathbin{\mathsf{sup}}\) introduced by Díaz-Caro and Dowek endows intuitionistic natural deduction with both harmonious and excessive rules, and its proof language forms the core of a quantum programming language. However, the resulting calculus is still permissive enough to express non-linear or genuinely non-physical operations: nothing in the type system enforces linearity or prevents the cloning of quantum data. In this paper we introduce a linear version of the \(\mathbin{\mathsf{sup}}\)-calculus. We separate classical and quantum data by means of a two-zone context discipline, and we restrict the use of the \(\mathbin{\mathsf{sup}}\)-connective and scalar combinations to ensure that well-typed quantum programs denote linear maps between finite-dimensional Hilbert spaces. We give a natural deduction style type system, an operational semantics with both deterministic and measurement steps, and we prove subject reduction and type soundness. We then show that no term in the purely quantum fragment can implement a duplicator \(\mathsf{qbit} \multimap \mathsf{qbit} \otimes \mathsf{qbit}\), while classical outcomes of measurements can still be duplicated freely. Finally, we sketch a denotational semantics in which closed quantum terms denote completely positive maps, and we relate our system to existing quantum \(\lambda\)-calculi.
Non-harmonious logical connectives have recently been shown to provide a natural proof-theoretic account of quantum measurement. In particular, the connective \(\mathbin{\mathsf{sup}}\) introduced by Díaz-Caro and Dowek endows intuitionistic natural deduction with both harmonious and excessive rules, and its proof language forms the core of a quantum programming language. However, the resulting calculus is still permissive enough to express non-linear or genuinely non-physical operations: nothing in the type system enforces linearity or prevents the cloning of quantum data. In this paper we introduce a linear version of the \(\mathbin{\mathsf{sup}}\)-calculus. We separate classical and quantum data by means of a two-zone context discipline, and we restrict the use of the \(\mathbin{\mathsf{sup}}\)-connective and scalar combinations to ensure that well-typed quantum programs denote linear maps between finite-dimensional Hilbert spaces. We give a natural deduction style type system, an operational semantics with both deterministic and measurement steps, and we prove subject reduction and type soundness. We then show that no term in the purely quantum fragment can implement a duplicator \(\mathsf{qbit} \multimap \mathsf{qbit} \otimes \mathsf{qbit}\), while classical outcomes of measurements can still be duplicated freely. Finally, we sketch a denotational semantics in which closed quantum terms denote completely positive maps, and we relate our system to existing quantum \(\lambda\)-calculi.
