Geometry of interaction
From Wikipedia, the free encyclopedia
The geometry of interaction (GoI) was introduced by Jean-Yves Girard as an operational interpretation of proofs. The idea of GoI is to replace global cut elimination steps with localised interactions. Similarly, GoI gives an interpretation of computer programs by modeling beta reduction as an interaction between terms. This proved useful in the study of optimal reduction strategies for the lambda calculus. Geometry of Interaction work had a strong influence on game semantics for linear logic and PCF. The most popular presentation of GoI is for the MELL fragment of linear logic.
Some of the main contributors to the field are Jean-Yves Girard, Samson Abramsky (foundational aspects), Radha Jagadeesan (foundational aspects), Phil Scott (categorical aspects), Esfandiar Hagheverdi (categorical aspects), Olivier Laurent (operational aspects) and Ian Mackie (applications).
[edit] External links
- Geometry of Interaction Workshop GEOCAL06, Marseille, January 2006 [1]
