The geometry of interaction of differential interaction nets

  • De Falco M
  • 6


    Mendeley users who have this article in their library.
  • 5


    Citations of this article.


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.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Marc De Falco

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free