Linear Realisability over Nets: Multiplicatives

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.

Authors

• Adrien Ragot
• Thomas Seiller
• Lorenzo Tortora de Falco

Keywords

• Linear Logic
• Proof Nets
• Realisability
• Orthogonality
• Hypergraphs
• Rewriting
• Correctness