A linear proof language for second-order intuitionistic linear logic
Logic in Computer Science
2024-06-19 v2 Logic
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.
Keywords
Cite
@article{arxiv.2310.08517,
title = {A linear proof language for second-order intuitionistic linear logic},
author = {Alejandro Díaz-Caro and Gilles Dowek and Malena Ivnisky and Octavio Malherbe},
journal= {arXiv preprint arXiv:2310.08517},
year = {2024}
}
Comments
arXiv admin note: substantial text overlap with arXiv:2201.11221