论文标题
线性线性lambda-calculus
A linear linear lambda-calculus
论文作者
论文摘要
我们为直觉乘法添加性线性逻辑的证明语言提供了线性定理，并结合了添加和标量乘法。从代数意义上讲，这种语言的证据是线性的。这项工作是更广泛的研究计划的一部分，旨在用形成量子编程语言的证明语言来定义逻辑。
We present a linearity theorem for a proof language of intuitionistic multiplicative additive linear logic, incorporating addition and scalar multiplication. The proofs in this language are linear in the algebraic sense. This work is part of a broader research program aiming to define a logic with a proof language that forms a quantum programming language.
