  To recover a satisfactory system, many proposals have been made, starting from the one by Danos &amp; Regnier  (1995)  but we want to mention here the very elegant approach by Guerrini, Martini and Masini  (Guerrini et al. 2003),  that neatly shows the connection between two level proof systems for modal logic, proper proof nets for MELL, and optimal reduction in the \(\lambda\)-calculus.