The Geometry of Interaction of Differential Interaction Nets
| dc.creator | de Falco, Marc | |
| dc.date | 2008-04-09 | |
| dc.date.accessioned | 2026-07-07T09:31:18Z | |
| dc.date.available | 2026-07-07T09:31:18Z | |
| dc.description | The Geometry of Interaction purpose is to give a semantic of proofs or programs accounting for their dynamics. The initial presentation, translated as an algebraic weighting of paths in proofnets, led to a better characterization of the lambda-calculus optimal reduction. Recently Ehrhard and Regnier have introduced an extension of the Multiplicative Exponential fragment of Linear Logic (MELL) that is able to express non-deterministic behaviour of programs and a proofnet-like calculus: Differential Interaction Nets. This paper constructs a proper Geometry of Interaction (GoI) for this extension. We consider it both as an algebraic theory and as a concrete reversible computation. We draw links between this GoI and the one of MELL. As a by-product we give for the first time an equational theory suitable for the GoI of the Multiplicative Additive fragment of Linear Logic. | |
| dc.description | 20 pagee, to be published in the proceedings of LICS08 | |
| dc.identifier | https://arxiv.org/abs/0804.1435 | |
| dc.identifier | http://arxiv.org/abs/0804.1435 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/158408 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | Programming Languages | |
| dc.title | The Geometry of Interaction of Differential Interaction Nets | |
| dc.type | text |