A linear proof language for second-order intuitionistic linear logic
arXiv:2310.08517 · doi:10.1007/978-3-031-62687-6_2
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.
arXiv admin note: substantial text overlap with arXiv:2201.11221