Computer Science – Logic in Computer Science
Scientific paper
2008-04-09
Computer Science
Logic in Computer Science
20 pagee, to be published in the proceedings of LICS08
Scientific paper
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.
No associations
LandOfFree
The Geometry of Interaction of Differential Interaction Nets does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with The Geometry of Interaction of Differential Interaction Nets, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and The Geometry of Interaction of Differential Interaction Nets will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-574603