A Linear Proof Language for Second-Order Intuitionistic Linear Logic

Authors: Alejandro Díaz-Caro, Gilles Dowek, Malena Ivnisky & Octavio Malherbe.

Abstract:
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.

More information:
https://link.springer.com/chapter/10.1007/978-3-031-62687-6_2