On geometry of interaction for polarized linear logic

摘要

We present Geometry of Interaction (GoI) models for Multiplicative Polarized Linear Logic,rnMLLP, which is the multiplicative fragment of Olivier Laurent’s Polarized Linear Logic. Thisrnis done by uniformly adding multi-points to various categorical models of GoI. Multi-pointsrnare shown to play an essential role in semantically characterizing the dynamics of proofrnnetworks in polarized proof theory. For example, they permit us to characterize the keyrnfeature of polarization, focusing, as well as being fundamental to our construction ofrnconcrete polarized GoI models.