MELL proof-nets without boxes: thirty years later

on YouTube ↗18m

" summary

Claim: exponentials are encoded as fixed-point operators in a non-wellfounded sequent calculus whose coinductive proofs desequentialise into an infinite sequence of finite MALL proof-nets, removing promotion boxes. Construction uses unfolding/fixpoint rules (three-premise ! and ? nodes), generalized axioms and finite approximants; cut elimination becomes local and exponentials turn out canonical. Built system (infinitary MELL and its proof-nets) implements promotion by an inductive family of approximants and already supports the usual simply-typed lambda translation, though some sequents escape ordinary MELL.

AI-written summary · about

" chapters (13)

1. 0:00Proof-nets without boxes intro
2. 1:23MELL proof-nets need boxes
3. 3:10MLL proof-nets and cuts
4. 5:16Promotion boxes problems
5. 6:25Previous box removal attempts
6. 7:27Introducing infinitary MELL
7. 9:17Progressing condition and proofs
8. 10:40Properties of infinitary MELL
9. 11:24Constructing M proof-nets
10. 12:52Promotion in M proof-nets
11. 13:58Lambda calculus translation
12. 14:41Summary and future
13. 16:09Q&A