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.
Ragot, A., Seiller, T., TORTORA DE FALCO, L. (2025). Linear Realisability over nets: multiplicatives. In leibniz international proceedings in informatics. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing [10.4230/LIPIcs.CSL.2025.43].
Linear Realisability over nets: multiplicatives
Ragot Adrien;Tortora de Falco Lorenzo
2025-01-01
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.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
