We provide the first proof of confluence for cut elimination in multiplicative-exponential linear logic proof-nets that is not based on Newman's lemma or strong normalization, not even indirectly. To achieve our goal, we take inspiration from Tait and Martin-Lof's method based on parallel reduction for the lambda-calculus, even though the wilder realm of untyped proof-nets makes the proof subtler and more challenging.
Guerrieri, G., Manara, G., TORTORA DE FALCO, L., Vaux Auclair, L. (2024). Confluence for Proof Nets via Parallel Cut Elimination. In Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp.464-483).
Confluence for Proof Nets via Parallel Cut Elimination
Giulio Guerrieri;Giulia Manara;Lorenzo Tortora de Falco;
2024-01-01
Abstract
We provide the first proof of confluence for cut elimination in multiplicative-exponential linear logic proof-nets that is not based on Newman's lemma or strong normalization, not even indirectly. To achieve our goal, we take inspiration from Tait and Martin-Lof's method based on parallel reduction for the lambda-calculus, even though the wilder realm of untyped proof-nets makes the proof subtler and more challenging.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
