Enhancing a Hierarchical Graph Rewriting Language Based on MELL Cut Elimination

This conference talk explores how hierarchical graph rewriting language LMNtal can be extended based on Multiplicative Exponential Linear Logic (MELL) cut elimination principles. Discover how researchers Kento Takyu and Kazunori Ueda from Waseda University enhance LMNtal to support operations on Promotion Boxes of MELL proof nets, creating a practical graph rewriting language with strong affinity to MELL proof nets. The presentation demonstrates how this extended language can encode other established concurrency models and how the LMNtal toolchain enables state-space search and model checking for MELL proof nets. The talk showcases the implementation of cut elimination rules and positions the platform as a valuable workbench for proof nets research. Presented at the 27th International Symposium on Practical Aspects of Declarative Languages (PADL'25), this 26-minute talk is sponsored by ACM SIGPLAN.