We present a polymorphic linear lambda-calculus as a proof language for second-order intuitionistic linear logic. The calculus includes addition and scalar multiplication, enabling the proof of a linearity result at the syntactic level.

翻译：我们提出一种多态线性λ演算，作为二阶直觉线性逻辑的证明语言。该演算包含加法与标量乘法运算，从而能够在语法层面证明线性性质。