MELL Proof-Nets Without Boxes: Thirty Years Later

Explore a novel approach to interpreting boxes in proof-nets during this conference talk on MELL proof-nets without boxes. Delve into the non-local nature of the promotion rule in sequent calculus and examine traditional methods of translation using promotion boxes. Discover why boxes are considered unsatisfactory due to their global computation steps and understand their role in resource sharing. Investigate various techniques for eliminating boxes and their respective computational interpretations. Learn about a new interpretation inspired by differential lambda calculus and fixed points in linear logic, where exponentials are encoded as fixed-point operators within a non-wellfounded sequent calculus. Examine how non-wellfounded proofs are desequentialized into infinite sequences of MALL proof-nets. Engage in a discussion about this innovative formalism and contemplate its potential computational power.