Geometry of interaction

Geometry of interaction

The Geometry of Interaction (GoI) was introduced by Jean-Yves Girard shortly after his seminal work on Linear Logic. In Linear Logic proofs can be seen as some kind of networks instead of the flat tree structure of Sequent calculus. To distinguish the real Proof nets from all the possible networks, Girard devised a criterium involving trips in the network. Trips can in fact be seen as some kind of operators acting on the proof. Drawing from this observation, Girard described directly this operator from the proof and has given a formula, the so-called "Execution formula", encoding the process of cut elimination at the level of operators.

At the same time, Lamping had given a hard to understand algorithm to compute the optimal reduction strategy for the lambda calculus. Gonthier, Abadi and Levy have further shown that GoI allows better analysis of Lamping's algorithm. This work on the lambda calculus has been independently carried by Danos and Regnier, Asperti and Guerrini. GoI work had a strong influence on game semantics for linear logic and PCF.

External links

* GoI tutorial given at Siena 07 by Laurent Regnier, in the Linear Logic workshop, [http://iml.univ-mrs.fr/~regnier/articles/siena07.pdf]


Wikimedia Foundation. 2010.

Игры ⚽ Поможем написать реферат

Look at other dictionaries:

  • Projective geometry — is a non metrical form of geometry, notable for its principle of duality. Projective geometry grew out of the principles of perspective art established during the Renaissance period, and was first systematically developed by Desargues in the 17th …   Wikipedia

  • Differential geometry of surfaces — Carl Friedrich Gauss in 1828 In mathematics, the differential geometry of surfaces deals with smooth surfaces with various additional structures, most often, a Riemannian metric. Surfaces have been extensively studied from various perspectives:… …   Wikipedia

  • Greek arithmetic, geometry and harmonics: Thales to Plato — Ian Mueller INTRODUCTION: PROCLUS’ HISTORY OF GEOMETRY In a famous passage in Book VII of the Republic starting at Socrates proposes to inquire about the studies (mathēmata) needed to train the young people who will become leaders of the ideal… …   History of philosophy

  • Social geometry — is a theoretical strategy of sociological explanation, invented by Donald Black, which uses a multi dimensional model to explain variations in the behavior of social life. In Black s own use and application of the idea, social geometry is an… …   Wikipedia

  • Fundamental interaction — In physics, a fundamental interaction or fundamental force is a mechanism by which particles interact with each other, and which cannot be explained in terms of another interaction. Overview In the conceptual model of fundamental interactions,… …   Wikipedia

  • List of combinatorial computational geometry topics — enumerates the topics of computational geometry that states problems in terms of geometric objects as discrete entities and hence the methods of their solution are mostly theories and algorithms of combinatorial character.See List of numerical… …   Wikipedia

  • Valency interaction formula — The Valency Interaction Formula, or VIF is a method for drawing molecular structural formulas based in quantum mechanics. The mathematical basis for VIF was formulated by Oktay Sinanoglu in a series of five papers published in 1984. [ Sinanoğlu,… …   Wikipedia

  • List of mathematics articles (G) — NOTOC G G₂ G delta space G networks Gδ set G structure G test G127 G2 manifold G2 structure Gabor atom Gabor filter Gabor transform Gabor Wigner transform Gabow s algorithm Gabriel graph Gabriel s Horn Gain graph Gain group Galerkin method… …   Wikipedia

  • Jean-Yves Girard — Pour les articles homonymes, voir Girard. Jean Yves Girard, né en 1947 à Lyon, est un logicien et mathématicien contemporain, directeur de recherche au CNRS au département de logique de la programmation de l institut de mathématiques de Luminy.… …   Wikipédia en Français

  • Samson Abramsky — Professor Samson Abramsky FRS is a computer scientist. Since the Year 2000, he has been a Fellow of the Royal Society of Edinburgh, a Fellow of Wolfson College, Oxford and Christopher Strachey Professor of Computing at Oxford University Computing …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”