Back to Search Start Over

A linear proof language for second-order intuitionistic linear logic

Authors :
Díaz-Caro, Alejandro
Dowek, Gilles
Ivnisky, Malena
Malherbe, Octavio
Source :
(WoLLIC 2024) - LNCS 14672:18-35, 2024
Publication Year :
2023

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.<br />Comment: arXiv admin note: substantial text overlap with arXiv:2201.11221

Subjects

Subjects :
Computer Science - Logic in Computer Science
Mathematics - Logic

Details

Database :
arXiv
Journal :
(WoLLIC 2024) - LNCS 14672:18-35, 2024
Publication Type :
Report
Accession number :
edsarx.2310.08517
Document Type :
Working Paper
Full Text :
https://doi.org/10.1007/978-3-031-62687-6_2
Full Text Access
View/download PDF

Tools

Authors Abstract Subjects Details