Linear logic without boxes
- 2 January 2003
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 223-234
- https://doi.org/10.1109/lics.1992.185535
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 logicKeywords
This publication has 6 references indexed in Scilit:
- Operational aspects of linear lambda calculusPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- From proof nets to interaction netsPublished by Cambridge University Press (CUP) ,1995
- Computational interpretations of linear logicTheoretical Computer Science, 1993
- The geometry of optimal lambda reductionPublished by Association for Computing Machinery (ACM) ,1992
- An algorithm for optimal lambda calculus reductionPublished by Association for Computing Machinery (ACM) ,1990
- Linear logicTheoretical Computer Science, 1987