## Paper: Linear logic without boxes (at LICS 1992)

**Georges Gonthier Martín Abadi Jean-Jacques Lévy**

### Abstract

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 λ-calculus implementations; computation is performed by simple graph rewriting. This graph implementation helps in understanding optimal reductions in the λ-calculus and in the various programming languages inspired by linear logic

### BibTeX

@InProceedings{Lvy-Linearlogicwithoutb, author = {Georges Gonthier and Martín Abadi and Jean-Jacques Lévy}, title = {Linear logic without boxes}, booktitle = {Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992)}, year = {1992}, month = {June}, pages = {223--234}, location = {Santa Cruz, CA, USA}, publisher = {IEEE Computer Society Press} }