MELL-Nets-in-LMNtal

Encoding of MELL(Multiplicative Exponential Linear Logic) cut-elimination into LMNtal.

This is the part of the presentation at APLAS2023.

demo

The visualization of the cut-elimination (corresponding to $\beta$-reduction) of a net obtained from a simply-typed $\lambda$ term: $(\lambda f: n \to n . \lambda x: n . f x)(\lambda x : n . x)$ by using our LMNtal visual tool:

The state space of this reduction:

Quick start

1. Install LaViT(LMNtal IDE) at https://www.ueda.info.waseda.ac.jp/lmntal/lavit/index.php?Download .
2. Open /lmntal/MELL-nets.lmn on LaViT.
3. Push the button of "Graphene" and you can see the visualization of the reduction.
4. Push the button of "StateViewer" and you can see the state space.