Publication year

On Geometry of Interaction

Resource type
Authors/contributors
Title
On Geometry of Interaction
Abstract
The paper expounds geometry of interaction, for the first time in the full case, i.e. for all connectives of linear logic, including additives and constants. The interpretation is done within a C*-algebra which is induced by the rule of resolution of logic programming, and therefore the execution formula can be presented as a simple logic programming loop. Part of the data is public (shared channels) but part of it can be viewed as private dialect (defined up to isomorphism) that cannot be shared during interaction, thus illustrating the theme of communication without understanding. One can prove a nilpotency (i.e. termination) theorem for this semantics, and also its soundness w.r.t. a slight modification of familiar sequent calculus in the case of exponential-free conclusions.
Date
1995
Proceedings Title
Proof and Computation
Place
Berlin, Heidelberg
Publisher
Springer
Pages
145-191
Series
NATO ASI Series
Language
en
DOI
10/fr557p
ISBN
978-3-642-79361-5
Library Catalog
Springer Link
Extra
ZSCC: NoCitationData[s0]
Citation
Girard, J.-Y. (1995). On Geometry of Interaction. In H. Schwichtenberg (Ed.), Proof and Computation (pp. 145–191). Berlin, Heidelberg: Springer. https://doi.org/10/fr557p
CATEGORICAL LOGIC
Processing time: 0.02 seconds

Graph of references

(from Zotero to Gephi via Zotnet with this script)
Graph of references