Masahiro HAMANO (PRESTO, Japan Science and Technology Agency)

A Geometry of Interaction for Polarized Linear Logic

We present a Geometry of Interaction (GoI) model for the multiplicative fragment (without structural rules) of Olivier Laurent's polarized linear logic. The problem of GoI peculiar to such logics is to semantically characterize the focalization property as well as the dynamics of cut-elimination.

Our GoI consists of the following two parts:

(i) A polarized GoI situation is presented by accommodating multi-points to a traced monoidal category. A key ingredient for the accommodation is uniformity of traces for multi-points. The setting, in which polarized proofs are interpreted, is a minimal categorical condition necessary to interpret polarized GoI, having the same spirit as the usual GoI situation a la Haghverdi-Scott. Execution formulas are defined over the interpretation of proofs and running the formulas is shown to characterize the focusing property as well as invariance of cut-elimination.

(ii) The Int construction (Joyal-Street-Verity '96) is investigated in the presence of categorical pullbacks. Our construction yields a compact version of Hamano-Scott's polarized category ('07) so that positive and negative monoidal categories arise which are contravariant to each other and whose forgetful functors to the original (compact closed) Int category have adjoints corresponding to the polarity changing operators.

A non-compact model is also presented inside an instance of (ii) to the category of multi-pointed relations thanks to their unique decompositionality.

(This is joint work with Phil Scott.)