Linear logic without boxes
Georges Gonthier, M. Abadi, Jean-Jacques Lévy · 2003
J.-Y. Girard's original definition of proof nets for linear logic involves boxes. The box is the unit for erasing and duplicating fragments of proof nets. It imposes synchronization, limits sharing, and impedes a completely local view of computation. The authors describe an implementation of proof nets without boxes. Proof nets are translated into graphs of the sort used in optimal lambda -calculus implementations; computation is performed by simple graph rewriting. This graph implementation helps in understanding optimal reductions in the lambda -calculus and in the various programming languages inspired by linear logic.>