Skip to content

Latest commit

 

History

History
23 lines (13 loc) · 1.06 KB

README.md

File metadata and controls

23 lines (13 loc) · 1.06 KB
Raw

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:

demo

The state space of this reduction:

demo

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.