Confluence for Proof-Nets via Parallel Cut Elimination
Giulio Guerrieri, Giulia Manara, Lorenzo Tortora de Falco, Lionel Vaux · EPiC series in computing · 2024
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.