On Context Semantics for Interaction Nets

ABSTRACT. Context semantics is a tool inspired by Girard' s geometry of interaction. It has had many applications from study of optimal reduction to proofs of complexity bounds. However, context semantics have been defined only on lambda-calculus and linear logic. In order to study other languages, in particular languages with more primitives (built-in arithmetics, pattern matching,…) we define a context semantics for a broader framework: interaction nets. These are a well-behaved class of graph rewriting systems. Here, two applications are explored. First, we define a notion of weight, based on context semantics paths, which bounds the length of reduction of nets. This could be used to prove strong complexity bounds for interaction net systems. Then, we define a denotational semantics for a large class of interaction net systems.