Differential interaction nets

Resource type
Authors/contributors
Title
Differential interaction nets
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.
Publication
Theoretical Computer Science
Volume
364
Issue
2
Pages
166-195
Date
November 6, 2006
Series
Logic, Language, Information and Computation
Journal Abbr
Theoretical Computer Science
Language
en
DOI
10/bg5g4b
ISSN
0304-3975
Accessed
2019-11-28T16:33:46Z
Library Catalog
ScienceDirect
Extra
ZSCC: 0000146
Citation
Ehrhard, T., & Regnier, L. (2006). Differential interaction nets. Theoretical Computer Science, 364(2), 166–195. https://doi.org/10/bg5g4b
DIFFERENTIAL CALCULUS
Processing time: 0.02 seconds

Graph of references

(from Zotero to Gephi via Zotnet with this script)
Graph of references