arxiv: 2605.14476 · v1 · submitted 2026-05-14 · 💻 cs.LO

Recognition: no theorem link

Proof Nets for PiL (Full Version)

Matteo Acclavio , Giulia Manara

Authors on Pith no claims yet

Pith reviewed 2026-05-15 01:51 UTC · model grok-4.3

classification 💻 cs.LO

keywords proof netsPiLpi-calculuslinear logicsequent calculuscorrectness criterionsequentializationcanonical representation

0 comments

The pith

Proof nets provide a canonical representation of sequent calculus derivations in PiL modulo rule permutations.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces proof nets for PiL, an extension of first-order multiplicative additive linear logic that adds operators to encode pi-calculus processes directly as formulas. It supplies a correctness criterion for the nets, a sequentialization procedure to recover sequent proofs from them, and an algorithm for translating derivations into nets. The central result is that these nets abstract away the order of independent rules, so that derivations differing only by permutations become identical. A reader would care because the graphical form removes redundant sequencing choices while retaining the logical structure of the encoded processes.

Core claim

We show that proof nets provide a canonical representation of sequent calculus derivations modulo rule permutations. This is supported by a correctness criterion that identifies valid proof nets for PiL formulas, a sequentialization procedure that reconstructs sequent derivations from the nets, and a translation algorithm from sequent proofs to nets that preserves the encoding of pi-calculus processes.

What carries the argument

The proof net correctness criterion together with the sequentialization procedure, which together ensure that nets capture exactly the equivalence class of derivations under rule permutations.

If this is right

Derivations differing only by permutation of independent rules correspond to identical proof nets.
The shallow encoding of pi-calculus processes into PiL formulas is preserved under translation to and from proof nets.
Proof equivalence modulo permutations can be checked by comparing the corresponding proof nets.
Sequentialization recovers a valid sequent proof from any correct proof net.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The canonical nets could reduce the search space when checking equivalences between pi-calculus processes by treating permutable steps as identical.
Similar net constructions might apply directly to other process calculi that admit shallow logical encodings.
The graphical form may make it easier to detect deadlocks or communication patterns that are obscured by linear sequent order.

Load-bearing premise

The new operators of PiL correctly and shallowly encode pi-calculus processes as formulas while preserving the logical properties of the base linear logic system.

What would settle it

A sequent derivation in PiL that translates to a proof net failing the correctness criterion, or two derivations differing by more than rule permutations that map to the same net.

Figures

Figures reproduced from arXiv: 2605.14476 by Giulia Manara, Matteo Acclavio.

**Figure 1.** Figure 1: Sequent calculus rules of PiL, where † := 𝑥 ∉ free(Γ). combination of the rules Иload and Иpop (resp. Яload and Яpop), together with the linear control of resources of the conjunction rules, guarantees that each nominal variable can be used as witness for at most one nominal quantification. Notation 22. We write ⊢PiL Γ to denote the existence of a derivation in PiL with conclusion the judgement ∅ ⊢ Γ. We d… view at source ↗

**Figure 2.** Figure 2: Coalescence steps for PiL. Proof. We define {{D}}co = ⟨𝜏(D), 𝛿D⟩ by translating top-down the rules of D using the construction in [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗

**Figure 3.** Figure 3: Translation of a derivation in PiL into a conflict net, with r 1 ∈ {`, ⊕, ∀, И, Я ◦ , Иload, Яload}, and r 2 ∈ {⊗, ◀}, and where we denote by D𝑥 (resp. 𝑎𝑥) the derivation (resp. link) obtained from D𝑦 (resp. 𝑎𝑦) by replacing all occurrences of the variable 𝑦 involved in the rule r ∈ {∃, ∇pop} with 𝑥 and where 𝛿 D 𝑎𝑥 = [𝑦/𝑥]𝛿 D𝑦 𝑎𝑦 if 𝑎𝑥 ≠ 𝑎𝑦 and 𝛿 D𝑦 𝑎𝑦 otherwise. Proof. The right-to-left implication is c… view at source ↗

**Figure 4.** Figure 4: Effect of coalescence steps in Figure 2 on coco-trees with leaves labeled [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗

**Figure 5.** Figure 5: Convergence of the non-trivial critical pair for flattening. [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗

**Figure 6.** Figure 6: Rule permutations in PiL with 𝛽, 𝛽1, 𝛽2 ∈ {⊗, ◀} and with 𝛼, 𝛼1, 𝛼2 ∈ {`, ⊕, ∃, ∀, И ◦ , Я ◦ , Иpop, Яpop, Иload, Яload}. as shown below. 𝑎1 . . . 𝑎𝑖 𝑎𝑖+1 . . . 𝑎𝑛 # 𝑏1 . . . 𝑏𝑚 # 𝑏1 . . . 𝑏𝑚 ⌢ ⌢ # ⇒⇒ 𝑎1 𝑏1 . . . 𝑏𝑚 𝑎𝑛 𝑏1 . . . 𝑏𝑚 ⌢ . . . ⌢ # We can now conclude the proof of the main result of this section, which states that slice nets are sound and complete for PiL. Theorem 3. Let Γ be a sequent. Then ⊢Pi… view at source ↗

read the original abstract

We introduce proof nets for PiL, an extension of first-order multiplicative additive linear logic with new operators allowing a shallow encoding of processes in the {\pi}-calculus as formulas. We provide correctness criterion, sequentialization procedure, and a proof translation algorithm. We show that proof nets provide a canonical representation of sequent calculus derivations modulo rule permutations.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper builds a proof-net system for PiL with its own operators, criterion, sequentialization, and translation, but the canonicity claim needs the full proofs to confirm the criterion handles every interaction with the new operators.

read the letter

The paper introduces proof nets for PiL, which extends first-order MALL with new operators that encode π-calculus processes as formulas. It supplies a correctness criterion, a sequentialization procedure that turns nets back into sequent derivations, and a translation algorithm. The authors claim these nets give a canonical representation of derivations modulo rule permutations. This setup is new; it does not reduce to existing proof-net systems for plain MALL, and the PiL-specific syntax and procedures are presented as fresh constructions. The work does a clear job defining the operators and laying out the three main procedures in one place. If the details hold, it offers a graphical tool that could link proof theory directly to process algebra. The soft spot is the completeness of the criterion. The central claim requires that every valid sequent derivation, including those using the new operators, sequentializes to a net and that permutation-equivalent derivations produce the same net. The abstract states the results but gives no sample derivations or explicit checks for how the new operators interact with the multiplicative and additive rules. If those interactions create cases the criterion misses, then distinct permutation classes could map to different nets or invalid nets could be accepted. The full manuscript must show that the procedures cover the PiL cases without gaps. This paper is for readers who already work with proof nets in linear logic and want to see them applied to concurrency calculi. Someone familiar with MALL proof nets will follow the extensions without much trouble. It deserves a serious referee because the constructions are concrete and the topic sits at a useful intersection, even though the proofs will need close inspection for completeness on the new operators. I would send it to peer review.

Referee Report

2 major / 2 minor

Summary. The paper introduces proof nets for PiL, an extension of first-order multiplicative-additive linear logic (MALL) with new logical operators that allow a shallow encoding of π-calculus processes as formulas. It supplies a correctness criterion, a sequentialization procedure, and a translation algorithm from sequent calculus derivations to these nets. The central claim is that the resulting proof nets constitute a canonical representation of sequent derivations modulo rule permutations, including those involving the new PiL operators.

Significance. If the constructions are complete and sound, the work would extend the graphical syntax of proof nets to a logic that directly encodes concurrent processes, offering a potential bridge between proof theory and process calculi. The explicit provision of a correctness criterion, sequentialization procedure, and translation algorithm constitutes a concrete technical contribution that could be verified or reused in related systems.

major comments (2)

[§3.2] §3.2, Definition 4 (correctness criterion): the criterion is formulated for the extended signature, but the paper does not exhibit a proof that every valid PiL sequent derivation (including those in which a new PiL operator is principal in an additive or cut rule) satisfies the criterion and sequentializes. Without such a completeness argument, the canonicity claim for all permutation classes remains open.
[§4.1] §4.1, Algorithm 1 (translation): the algorithm is stated to commute with rule permutations, yet no induction is supplied showing that permutations involving the new PiL operators produce identical nets. A single counter-example derivation using a new operator whose permutation class maps to distinct nets would falsify the central claim.

minor comments (2)

[§2] Notation for the new PiL operators is introduced without a consolidated table comparing them to the original MALL connectives; a small table in §2 would improve readability.
[Figure 3] Figure 3 (example net) uses an abbreviation for the sequentialization steps that is not defined until the caption of Figure 4; move the definition earlier or add a cross-reference.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. We appreciate the acknowledgment of the potential bridge between proof theory and process calculi. We address each major comment below and will revise the manuscript accordingly to strengthen the completeness arguments.

read point-by-point responses

Referee: [§3.2] §3.2, Definition 4 (correctness criterion): the criterion is formulated for the extended signature, but the paper does not exhibit a proof that every valid PiL sequent derivation (including those in which a new PiL operator is principal in an additive or cut rule) satisfies the criterion and sequentializes. Without such a completeness argument, the canonicity claim for all permutation classes remains open.

Authors: We agree that an explicit completeness proof is required to confirm that every sequent derivation in PiL, including those with new PiL operators principal in additive or cut rules, satisfies the correctness criterion and sequentializes back to a derivation. The manuscript establishes that the translation produces correct nets and that sequentialization works for the cases considered, but we acknowledge the need for a dedicated argument covering all permutation classes involving the new operators. We will add this completeness proof, most likely as an expanded subsection in §3.2. revision: yes
Referee: [§4.1] §4.1, Algorithm 1 (translation): the algorithm is stated to commute with rule permutations, yet no induction is supplied showing that permutations involving the new PiL operators produce identical nets. A single counter-example derivation using a new operator whose permutation class maps to distinct nets would falsify the central claim.

Authors: We agree that the claim of canonicity requires an explicit inductive argument showing invariance under permutations that involve the new PiL operators. The manuscript presents the translation algorithm and argues that it yields a canonical representation, but does not include the full induction for these specific cases. We will supply the missing induction in the revised version of §4.1, proving that any two derivations related by permutations of rules with PiL operators translate to the same proof net. revision: yes

Circularity Check

0 steps flagged

No circularity: canonicity proved via independent correctness criterion and sequentialization for the PiL extension

full rationale

The paper defines new PiL operators, supplies an explicit correctness criterion, sequentialization procedure, and translation algorithm from sequent calculus to proof nets, then claims to prove that nets are canonical modulo rule permutations. These steps are presented as new constructions whose properties (including completeness for derivations using the added operators) are established by direct argument rather than by reducing to a fitted parameter, self-citation chain, or definitional equivalence. No load-bearing step equates the target canonicity result to its own inputs by construction, and the derivation remains self-contained against the stated external benchmarks of MALL proof-net theory.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The constructions rest on the standard sequent rules and cut-elimination properties of first-order MALL together with the syntactic definition of the new PiL operators.

axioms (1)

standard math Standard sequent calculus rules and cut-elimination for first-order multiplicative additive linear logic
PiL is defined as an extension of this established base system.

invented entities (1)

New logical operators of PiL no independent evidence
purpose: To permit shallow encoding of π-calculus processes as formulas
These operators are introduced syntactically in the paper; no independent semantic evidence is supplied in the abstract.

pith-pipeline@v0.9.0 · 5334 in / 1170 out tokens · 58987 ms · 2026-05-15T01:51:40.131376+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

32 extracted references · 32 canonical work pages · 1 internal anchor

[1]

An- nals of Pure and Applied Logic101(1), 29–64 (1999)

Abrusci, V., Ruet, P.: Non-commutative logic I: the multiplicative fragment. An- nals of Pure and Applied Logic101(1), 29–64 (1999). https://doi.org/https:// doi.org/10.1016/S0168-0072(99)00014-7, https://www.sciencedirect.com/science/ article/pii/S0168007299000147

work page doi:10.1016/s0168-0072(99)00014-7 1999
[2]

In: Fernández, M., Muscholl, A

Acclavio, M., Maieli, R.: Generalized connectives for multiplicative linear logic. In: Fernández, M., Muscholl, A. (eds.) 28th EACSL Annual Conference on Com- puter Science Logic (CSL 2020). LIPIcs, vol. 152, pp. 6:1–6:16. Schloss Dagstuhl– Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2020). https://doi.org/10. 4230/LIPIcs.CSL.2020.6, https://drops...

work page 2020
[3]

In: Vafeiadis, V

Acclavio, M., Manara, G., Montesi, F.: Formulas as processes, deadlock-freedom as choreographies. In: Vafeiadis, V. (ed.) Programming Languages and Systems. pp. 23–55. Springer Nature Switzerland, Cham (2025)

work page 2025
[4]

Acclavio, M., Manara, G., Montesi, F.: Formulas as processes, deadlock-freedom as choreographies (extended version) (2025), https://arxiv.org/abs/2501.08928

work page arXiv 2025
[5]

Mathe- matical Structures in Computer Science7(6), 663–669 (1997)

Bellin, G.: Subnets of proof-nets in multiplicative linear logic with mix. Mathe- matical Structures in Computer Science7(6), 663–669 (1997)

work page 1997
[6]

Danos, V.: La Logique Linéaire appliquée à l’étude de divers processus de normali- sation (principalement du Lambda-calcul). Ph.D. thesis, Université Paris 7 (1990), http://www.theses.fr/1990PA077188, thèse de doctorat dirigée par Girard, Jean- Yves Mathématiques Paris 7 1990 6 In this setting, an axiomatic linkingΛonΓconsists of links of the form {𝑃(𝑡 1,...

work page 1990
[7]

Archive for Mathematical logic28(3), 181–203 (1989)

Danos, V., Regnier, L.: The structure of multiplicatives. Archive for Mathematical logic28(3), 181–203 (1989). https://doi.org/10.1007/BF01622878

work page doi:10.1007/bf01622878 1989
[8]

Talk at TLLA 2025: 17th International Workshop on the Theory and Applications of Linear Logic and Related Topics (2025), https://lipn.univ-paris13

Fiorillo, L., Osorio-Valencia, J., Saurin, A.: On correctness, sequentialization and interpolation. Talk at TLLA 2025: 17th International Workshop on the Theory and Applications of Linear Logic and Related Topics (2025), https://lipn.univ-paris13. fr/TLLA/2025/abstracts/14-fiorillo-osoriovalencia-saurin.pdf

work page 2025
[9]

Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable bind- ing. Form. Asp. Comput.13(3–5), 341–363 (jul 2002). https://doi.org/10.1007/ s001650200016, https://doi.org/10.1007/s001650200016

work page doi:10.1007/s001650200016 2002
[10]

Linear logic , journal =

Girard, J.Y.: Linear logic. Theoretical Computer Science50(1), 1–101 (1987). https://doi.org/10.1016/0304-3975(87)90045-4

work page doi:10.1016/0304-3975(87)90045-4 1987
[11]

In: Ursini, A., Agliano, P

Girard, J.Y.: Proof-nets : the parallel syntax for proof-theory. In: Ursini, A., Agliano, P. (eds.) Logic and Algebra. Marcel Dekker, New York (1996)

work page 1996
[12]

NATO ASI Series F Computer and Systems Sciences175, 183–212 (2000)

Girard, J.Y.: On the meaning of logical rules II: multiplicatives and additives. NATO ASI Series F Computer and Systems Sciences175, 183–212 (2000)

work page 2000
[13]

In: Geuvers, H

Heijltjes, W.B., Hughes, D.J.D., Straßburger, L.: Proof Nets for First-Order Ad- ditive Linear Logic. In: Geuvers, H. (ed.) 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), vol. 131, pp. 22:1–22:22. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dags...

work page doi:10.4230/lipics.fscd.2019.22 2019
[14]

Hughes, D.: First-order proofs without syntax (2014), berkeley Logic Colloquium

work page 2014
[15]

In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

Hughes, D., Heijltjes, W.: Conflict nets: Efficient locally canonical mall proof nets. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. p. 437–446. LICS ’16, Association for Computing Machin- ery, New York, NY, USA (2016). https://doi.org/10.1145/2933575.2934559, https: //doi.org/10.1145/2933575.2934559

work page doi:10.1145/2933575.2934559 2016
[16]

Hughes, D.J.D.: Abstract p-time proof nets for mall: Conflict nets (2008), https: //arxiv.org/abs/0801.2421

work page internal anchor Pith review Pith/arXiv arXiv 2008
[17]

In: Proceed- ings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Hughes, D.J.D.: Unification nets: canonical proof net quantifiers. In: Proceed- ings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. p. 540–549. LICS ’18, Association for Computing Machinery, New York, NY, USA (2018). https://doi.org/10.1145/3209108.3209159, https://doi.org/10.1145/ 3209108.3209159

work page doi:10.1145/3209108.3209159 2018
[18]

In: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

Hughes, D.J.D., Straßburger, L., Wu, J.H.: Combinatorial proofs and decomposi- tion theorems for first-order logic. In: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–13 (2021). https://doi.org/10.1109/ LICS52264.2021.9470579

work page arXiv 2021
[19]

ACM Trans

Hughes, D.J.D., Van Glabbeek, R.J.: Proof nets for unit-free multiplicative- additive linear logic. ACM Trans. Comput. Logic6(4), 784–842 (oct 2005). https: //doi.org/10.1145/1094622.1094629, https://doi.org/10.1145/1094622.1094629

work page doi:10.1145/1094622.1094629 2005
[20]

Istituto di Elaborazione della Informazione, Consiglio Nazionale delle Ricerche (1976)

Martelli, A., Montanari, U.: Unification in linear time and space: A structured presentation. Istituto di Elaborazione della Informazione, Consiglio Nazionale delle Ricerche (1976)

work page 1976
[21]

Milner, R.: A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol. 92. Springer (1980). https://doi.org/10.1007/3-540-10235-3, https: //doi.org/10.1007/3-540-10235-3

work page doi:10.1007/3-540-10235-3 1980
[22]

Cambridge University Press (2023)

Montesi, F.: Introduction to Choreographies. Cambridge University Press (2023). https://doi.org/10.1017/9781108981491 20 M. Acclavio and G. Manara

work page doi:10.1017/9781108981491 2023
[23]

Nguyên, L.T.D., Straßburger, L.: A System of Interaction and Structure III: The Complexity of BV and Pomset Logic (2022), https://hal.inria.fr/hal-03909547, working paper or preprint

work page 2022
[24]

In: Manea, F., Simpson, A

Nguyên, L.T.D., Straßburger, L.: BV and Pomset Logic are not the same. In: Manea, F., Simpson, A. (eds.) 30th EACSL Annual Conference on Com- puter Science Logic (CSL 2022). Leibniz International Proceedings in Informat- ics (LIPIcs), vol. 216, pp. 3:1–3:17. Schloss Dagstuhl – Leibniz-Zentrum für In- formatik, Dagstuhl, Germany (2022). https://doi.org/10....

work page doi:10.4230/lipics.csl.2022.3 2022
[25]

The Review of Symbolic Logic17(4), 996–1017 (2024)

Nicolai, C., Piazza, M., Tesi, M.: Non-contractive logics, paradoxes, and mul- tiplicative quantifiers. The Review of Symbolic Logic17(4), 996–1017 (2024). https://doi.org/10.1017/S1755020323000138

work page doi:10.1017/s1755020323000138 2024
[26]

Informa- tion and Computation186(2), 165–193 (2003)

Pitts, A.M.: Nominal logic, a first order theory of names and binding. Informa- tion and Computation186(2), 165–193 (2003). https://doi.org/https://doi.org/ 10.1016/S0890-5401(03)00138-X, https://www.sciencedirect.com/science/article/ pii/S089054010300138X, theoretical Aspects of Computer Software (TACS 2001)

work page doi:10.1016/s0890-5401(03)00138-x 2003
[27]

Retoré, C.: Réseaux et Séquents Ordonnés. Ph.D. thesis, Université Paris VII (1993)

work page 1993
[28]

Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics pp

Retoré, C.: Pomset logic: The other approach to noncommutativity in logic. Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics pp. 299– 345 (2021)

work page 2021
[29]

Theoreti- cal Computer Science294(3), 473–488 (2003)

Retoré, C.: Handsome proof-nets: perfect matchings and cographs. Theoreti- cal Computer Science294(3), 473–488 (2003). https://doi.org/https://doi.org/ 10.1016/S0304-3975(01)00175-X, https://www.sciencedirect.com/science/article/ pii/S030439750100175X, linear Logic

work page doi:10.1016/s0304-3975(01)00175-x 2003
[30]

In: Fernández, M

Saurin, A.: Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation. In: Fernández, M. (ed.) 10th International Con- ference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), vol. 337, pp. 32:1– 32:21. Schloss Dagstuhl – Leibniz-Zentrum für Infor...

work page doi:10.4230/lipics.fscd.2025.32 2025
[31]

https://doi.org/10.2168/LMCS-2(2:4)2006

Tiu, A.F.: A system of interaction and structure II: The need for deep inference 2(2), 1–24 (2006). https://doi.org/10.2168/LMCS-2(2:4)2006

work page doi:10.2168/lmcs-2(2:4)2006 2006
[32]

Journal of Symbolic Logic55(1), 41–64 (1990)

Yetter, D.N.: Quantales and (noncommutative) linear logic. Journal of Symbolic Logic55(1), 41–64 (1990). https://doi.org/10.2307/2274953 Proof Nets for PiL (Full Version) 21 A Details of the proofs of Lemma 3 Lemma 5.LetPbe a conflict net such thatP 1 ← P − → P2 then there is a con- flict netP ′ such thatP 1 − →∗ P′ andP 2 − →∗ P′, and the derivations cor...

work page doi:10.2307/2274953 1990