APLAS 2023
Sun 26 - Wed 29 November 2023 Taipei, Taiwan

We show that several key language constructs of the hierarchical graph rewriting language LMNtal correspond directly to the operations required for the cut elimination of MELL (Multiplicative Exponential Linear Logic) Proof Nets, and that cut elimination of MELL can be succinctly encoded into LMNtal. We encoded and ran the cut elimination rules in LMNtal and demonstrated that the implementation serves as a workbench of MELL proof reduction.

Poster (latest) (poster_latest.pdf)448KiB
Extended Abstract (extended_abstract.pdf)733KiB