La Geometría de Interacción (GdI) fue presentada por Jean-Yves Girard poco después de su trabajo sobre lógica lineal . En lógica lineal, las pruebas pueden verse como varios tipos de redes en oposición a las estructuras de árbol plano del cálculo secuencial . Para distinguir las redes de prueba reales de todas las redes posibles, Girard ideó un criterio que involucra viajes en la red. De hecho, los viajes pueden verse como una especie de operador [ aclaración necesaria ] que actúa sobre la prueba. A partir de esta observación, Girard describió directamente este operador de la prueba y dio una fórmula, la llamada fórmula de ejecución , que codifica el proceso deEliminación de cortes a nivel de operadores.
Una de las primeras aplicaciones significativas de GoI fue un mejor análisis [1] del algoritmo de Lamping [2] para la reducción óptima del cálculo lambda . GoI tuvo una fuerte influencia en la semántica del juego para lógica lineal y PCF .
GoI se ha aplicado a la optimización profunda del compilador para cálculos lambda. [3] Se ha utilizado una versión limitada de GoI denominada Geometry of Synthesis para compilar lenguajes de programación de orden superior directamente en circuitos estáticos. [4]