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-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.
Mendeley saves you time finding and organizing research
Choose a citation style from the tabs below