Linear Realisability over nets: multiplicatives (long version)

2024/11/26 by Ragot, Adrien, Seiller, Thomas, de Falco, Lorenzo Tortora
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2411.17486

Abstract

We provide a new realisability model based on orthogonality for the multiplicative fragment of linear logic, both in presence of generalised axioms (MLL*) and in the standard case (MLL). The novelty is the definition of cut elimination for generalised axioms. We prove that our model is adequate and complete both for MLL* and MLL.

Related

• Elimination and cut-elimination in multiplicative linear logic
• Simple multiplicative proof nets with units
• The relational model is injective for Multiplicative Exponential Linear Logic
• A semantic account of strong normalization in Linear Logic
• A New Linear Time Correctness Condition for Multiplicative Linear Logic