Paper: Linear logic without boxes (at LICS 1992)
Authors: Gonthier, G. Abadi, M. Levy, J.-J.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{GonthierAbadiLevy-Linearlogicwithoutb, author = {Gonthier, G. and Abadi, M. and Levy, J.-J.}, title = {Linear logic without boxes}, booktitle = {Proceedings of the Seventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1992}, year = 1992, editor = {Andre Scedrov}, month = {June}, pages = {223--234}, location = {Santa Cruz, CA, USA}, publisher = {IEEE Computer Society Press} }