Differential interaction nets |
| |
Authors: | T Ehrhard L Regnier |
| |
Affiliation: | Institut de Mathémathiques de Luminy, Campus de Luminy, Case 907, 13288 Marseille Cedex 9, France |
| |
Abstract: | We introduce interaction nets for a fragment of the differential lambda-calculus and exhibit in this framework a new symmetry between the of course and the why not modalities of linear logic, which is completely similar to the symmetry between the tensor and par connectives of linear logic. We use algebraic intuitions for introducing these nets and their reduction rules, and then we develop two correctness criteria (weak typability and acyclicity) and show that they guarantee strong normalization. Finally, we outline the correspondence between this interaction nets formalism and the resource lambda-calculus. |
| |
Keywords: | Lambda-calculus Linear logic Differential lambda-calculus Interaction nets Resource lambda-calculus Lambda-calculus with multiplicities |
本文献已被 ScienceDirect 等数据库收录! |
|