2008 23rd Annual IEEE Symposium on Logic in Computer Science
The Geometry of Interaction of Differential Interaction Nets
June 24-June 27
ISBN: 978-0-7695-3183-0
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.
Index Terms:
geometry of interaction, differential interaction nets, linear logic, differential linear logic, sharing graphs
Citation:
Marc de Falco, "The Geometry of Interaction of Differential Interaction Nets," lics, pp.465-475, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, 2008