In proof theory, the Geometry of Interaction (GoI) was introduced by Jean-Yves Girard shortly after his work on linear logic.
In linear logic, proofs can be seen as various kinds of networks as opposed to the flat tree structures of sequent calculus.
Subsequent constructions by Girard proposed variants in which proofs are represented as flows,[2] or operators in von Neumann algebras.
Beyond the dynamic interpretation of proofs, geometry of interaction constructions provide models of linear logic, or fragments thereof.
[8] A bounded version of GoI dubbed the Geometry of Synthesis has been used to compile higher-order programming languages directly into static circuits.