Proof Nets for Intuitionistic Linear Logic: Essential Nets
François Lamarche · HAL (Le Centre pour la Communication Scientifique Directe) · 2008
We present a class of proof nets that are specially designed for Intuitionistic Linear Logic, for which we give a correctness criterion, as well as a cut-elimination procedure. The proof of sequentialization uses a special kind of oriented paths.