TY - CONF
TI - On Geometry of Interaction
AU - Girard, Jean-Yves
A2 - Schwichtenberg, Helmut
T3 - NATO ASI Series
AB - 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.
C1 - Berlin, Heidelberg
C3 - Proof and Computation
DA - 1995///
PY - 1995
DO - 10/fr557p
DP - Springer Link
SP - 145
EP - 191
LA - en
PB - Springer
SN - 978-3-642-79361-5
KW - Interactive semantics
KW - Linear logic
ER -
TY - JOUR
TI - Linear logic
AU - Girard, Jean-Yves
T2 - Theoretical Computer Science
AB - The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
DA - 1987/01/01/
PY - 1987
DO - 10/cmv5mj
DP - ScienceDirect
VL - 50
IS - 1
SP - 1
EP - 101
J2 - Theoretical Computer Science
LA - en
SN - 0304-3975
UR - http://www.sciencedirect.com/science/article/pii/0304397587900454
Y2 - 2019/11/26/21:07:06
KW - Denotational semantics
KW - Linear logic
KW - Type theory
ER -