The promotion rule is non-local in the sequent calculus; consequently, we need to impose some sequentiality to translate it into proof-nets. Traditionally, it has been done using a `promotion box’. However, boxes are unsatisfactory since they make global computation steps. Computationally, their role can be understood as an indicator and means of resource sharing. There are several ways to get rid of boxes, each with its own computational interpretation.

Inspired by a decade of work on differential lambda calculus and fixed points in linear logic, we propose a new way of interpreting boxes. We encode exponentials as fixed-point operators and consider their non-wellfounded sequent calculus. A non-wellfounded proof is desequentialised into an infinite sequence of MALL proof-nets. In this talk, we will discuss this new formalism and ponder upon its computational power.