Proof Nets for PiL (Full Version)
计算机科学中的逻辑
2026-05-15 v1
摘要
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.
引用
@article{arxiv.2605.14476,
title = {Proof Nets for PiL (Full Version)},
author = {Matteo Acclavio and Giulia Manara},
journal= {arXiv preprint arXiv:2605.14476},
year = {2026}
}