A categorical approach to linear logic, geometry of proofs and full completeness

The major contributions of this thesis are in the areas of Geometry of Interaction (GoI) and full completeness for models of linear logic. Geometry of interaction was introduced by Girard in the late 80's. It provides a new semantics of computation that captures the dynamical aspects of computation; a feature which is missing in denotational semantics. Subsequently Abramsky and Jagadeesan introduced a categorical interpretation of this program using domain theoretical categories. Recently Abramsky introduced a general categorical GoI construction which leads to models of computation (combinatory algebras) based on GoI Situations that essentially consist of a traced symmetric monoidal category with additional structure.;In this thesis we develop this general programme in all details. We also prove that this construction can be done in a more general framework, namely based on symmetric monoidal closed categories.;We also introduce a class of categories, called unique decomposition categories (UDC), that axiomatise the so-called particle-style GoI along with providing a computational calculus. Unique decomposition categories are motivated by and generalise the partially additive categories of Manes and Arbib. These models are special cases of the general construction which capture an important class of examples. They provide us with dataflow-like computational analysis.;We also establish connections with the work of Girard/Danos/Regnier on dynamic algebras. This formalises the path-based approach to GoI, the so-called path-semantics. The paths in proof-nets used in the work of Danos/Regnier correspond to morphisms in UDC-based models.;Full completeness for models of linear logic was introduced and studied by Abramsky and Jagadeesan. Full completeness establishes the tightest connection between syntax and semantics: it is completeness with respect to proofs instead of the traditional completeness with respect to provability. Recently Hyland and his student Tan introduced the double glueing method in Tan's PhD thesis. Tan's work provides the first steps towards an axiomatic approach to full completeness problems for linear logic.;In this thesis we construct a class of models for the multiplicative fragment of linear logic with the MIX rule, based on partially additive categories together with the Int construction of Joyal, Street and Verity and the double glueing construction. We also prove that such models are fully complete for the multiplicative fragment of linear logic with the MIX rule.