# Geometry of interaction

(Difference between revisions)
This was a striking novelty as it was the first time that a mathematical model of logic (lambda-calculus) didn't interpret a proof of $A\limp B$ as a morphism from (the space interpreting) A to (the space interpreting) B and proof composition (cut rule) as the composition of morphisms. Rather the proof was interpreted as an operator acting on (the space interpreting) $A\limp B$, that is a morphism from $A\limp B$ to $A\limp B$. For proof composition the problem was then, given an operator on $A\limp B$ and another one on $B\limp C$ to construct a new operator on $A\limp C$. This problem was originally expressed as a feedback equation solved by the execution formula. The execution formula has some formal analogies with Kleene's formula for recursive functions, which allowed to claim that GoI was an operational semantics, as opposed to traditionnal denotational semantics.