Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
9655965 | Electronic Notes in Theoretical Computer Science | 2005 | 21 Pages |
Abstract
We analyze the categorical foundations of Girard's Geometry of Interaction Program for Linear Logic. The motivation for the work comes from the importance of viewing GoI as a new kind of semantics and thus trying to relate it to extant semantics. In an earlier paper we showed that a special case of Abramsky's GoI situations-ones based on Unique Decomposition Categories (UDC's)-exactly captures Girard's functional analytic models in his first GoI paper, including Girard's original Execution formula in Hilbert spaces, his notions of orthogonality, types, datum, algorithm, etc. Here we associate to a UDC-based GoI Situation a denotational model (a *- autonomous category (without units) with additional exponential structure). We then relate this model to some of the standard GoI models via a fully-faithful embedding into a double-gluing category, thus connecting up GoI with earlier Full Completeness Theorems.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Esfandiar Haghverdi, Philip Scott,