Despite being one of the most successful outcomes of linear logic, the theory of proof-nets for Multiplicative and Exponential Linear Logic (MELL) is not fully satisfactory. In this talk I will discuss two of its shortcomings, the need of explicit boxes, and the elaborated reasoning behind its proof of strong normalization. In the first part I will show how switching to a polarized version of MELL allows to internalize boxes, so that they are induced by the proof itself, instead of being explicitly added to the graph. These "implicit boxes" are canonical and enjoy a correctness criterion which is a natural extension of Laurent's criterion for Polarized MELL. Moreover, they induce new cut-elimination rules.

In the second part I will focus on the new dynamics recasted in the usual, non-polarized setting with explicit boxes. I will introduce a notion of substitution for proof nets and use it to revisit the proof of strong normalization, organizing it along three abstract principles. The new dynamics admits a very simple proof of these principles (and thus of strong normalization), while the ordinary dynamics does not.