A linear proof language for second-order intuitionistic linear logic
Voices Powered by
Connected to paperThis paper is a preprint and has not been certified by peer review
A linear proof language for second-order intuitionistic linear logic
Alejandro Díaz-Caro, Gilles Dowek, Malena Ivnisky, Octavio Malherbe
AbstractWe 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.