Name
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 |
Year | DOI | Venue |
|---|---|---|
1992 | 10.1109/LICS.1992.185535 | LICS |
Keywords | Field | DocType |
linear logic,graph implementation,proof nets,rewriting systems,lambda -calculus,theorem proving,formal logic,graph rewriting,encoding,geometry,computational modeling,lambda calculus,concrete,parallel processing,impedance,logic programming,linear programming,programming language,calculus | Discrete mathematics,Lambda calculus,Interaction nets,Computer science,Geometry of interaction,Proof calculus,Theoretical computer science,Noncommutative logic,Graph rewriting,Linear logic,Logic programming | Conference |
Citations | PageRank | References |
49 | 4.90 | 3 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Georges Gonthier | 1 | 2275 | 195.06 |
| Martín Abadi | 2 | 12074 | 1324.31 |
| Jean-jacques Lévy | 3 | 932 | 95.41 |