Eliminating infinitely many cuts in non-wellfounded MLL proof-nets

Non-wellfounded and circular proofs have been recognised over the past decade as a valuable tool to study logics expressing (co)inductive properties, e.g.-calculi. Such proofs are non-wellfounded sequent derivations together with a global validity condition expressed in terms of progressing threads. While the cut-free fragment of circular proofs is satisfactory, cuts are poorly treated and the non-canonicity of sequent proofs becomes a major issue in the non-wellfounded setting. The present paper develops the theory of infinets-proof-nets for non-wellfounded proofs-allowing infinets with infinitely many cuts therefore solving a crucial shortcoming of the previous work [21], characterising sequentialisation and proving a cut-elimination theorem. To that end, we provide an alternate cut reduction for non-wellfounded sequent calculus