Paper: Linear logic without boxes (at LICS 1992)

Authors: 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}
  }