Logic in Computer Science (LICS 1992)

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