From Proof Nets to Games
François Lamarche · Electronic Notes in Theoretical Computer Science · 1996
We give a class of proof nets for Intuitionistic Linear Logic with the connectives -o, !, prove a correctness criterion for them and show that a games semantics can be directly derived from these nets, along with a full completeness theorem.