We prove a linearity theorem for an extension of linear logic with addition and multiplication by a scalar: the proofs of some propositions in this logic are linear in the algebraic sense. This work is part of a wider research program that aims at defining a logic whose proof language is a quantum programming language.

翻译：我们证明了在线性逻辑中增加标量加法和乘法的线性性定理：该逻辑中某些命题的证明在代数意义上是线性的。这项工作是一项更广泛研究计划的一部分，该计划旨在定义一种证明语言即为量子编程语言的逻辑。