Sequentialization is as fun as bungee jumping

Rémi Di Guardia (1, 2) , Olivier Laurent (1, 2) , Lionel Vaux (3) , Lorenzo Tortora de Falco (4)

1 LIP - Laboratoire de l'Informatique du Parallélisme
2 PLUME - Preuves et Langages
3 I2M - Institut de Mathématiques de Marseille
4 Gruppo di Logica

We propose a new proof of sequentialization for the proof nets of unit-free multiplicative linear logic with mix. It is based on the search of a splitting parr by means of a simple new lemma about proof structures: the bungee jumping lemma.

Domaines: Logique en informatique [cs.LO]

Rémi Di Guardia, Olivier Laurent, Lionel Vaux, Lorenzo Tortora de Falco. Sequentialization is as fun as bungee jumping. 7th International Workshop on Trends in Linear Logic and Applications (TLLA 2023), Jul 2023, Rome Sapienza Universita di Roma, Italy. ⟨hal-04515300⟩