APLAS 2023 (series) / Student Research Competition and Posters /
[Non-SRC] Encoding MELL Cut Elimination into a Hierarchical Graph Rewriting Language
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 |