2026-07-25T09:51:03Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4051 2024-03-06T10:34:45Z ddc:004 open_access

Linear Logic and Strong Normalization Accattoli, Beniamino linear logic proof nets strong normalization explicit substitutions Strong normalization for linear logic requires elaborated rewriting techniques. In this paper we give a new presentation of MELL proof nets, without any commutative cut-elimination rule. We show how this feature induces a compact and simple proof of strong normalization, via reducibility candidates. It is the first proof of strong normalization for MELL which does not rely on any form of confluence, and so it smoothly scales up to full linear logic. Moreover, it is an axiomatic proof, as more generally it holds for every set of rewriting rules satisfying three very natural requirements with respect to substitution, commutation with promotion, full composition, and Kesner's IE property. The insight indeed comes from the theory of explicit substitutions, and from looking at the exponentials as a substitution device. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Beniamino Accattoli 2013 Is Part Of LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2013.39 urn:nbn:de:0030-drops-40515 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.39 eng https://creativecommons.org/licenses/by/3.0/legalcode