Esfandiar Haghverdi - Linear logic, geometry of proofs and full completeness

Girard invented Linear Logic, a resource sensitive logic which is a refinement of classical and intuitionistic logic. He introduced many novelties including a graphical proof syntax and a wide range of mathematical models. He also introduced his Geometry of Interaction Programme (GoI) in a series of papers. The goal of this programme was to provide a mathematical analysis of the cut elimination process in linear logic proofs. This new interpretation replaces graph-rewriting by information flow in proof-nets. A specific model considered by Girard was based on the C^*-algebra of bounded linear operators on the space . From a computational point of view this yields an analysis of -calculus -reduction and has been applied in such areas as the analysis of optimal reduction strategies. GoI has also brought forward a new perspective for the semantics of computation which places it in a kind of ``middle ground'' between imperative/procedural, denotational/operational approaches in the semantics of programming languages. This new view helps to model the computational dynamics which is absent in denotational semantics and manages to offer a mathematical analysis which is lacking in operational semantics.

In this talk we give a general algebraic framework for the Girard programme inspired by recent work of Samson Abramsky. We introduce a special class of traced symmetric monoidal categories called traced unique decomposition categories. We discuss how to construct models of linear logic based on such categories that we call GoI-models. We also show that such models are fully complete, that is completeness with respect to proofs. Next, we define type-free GoI-models and discuss how these provide a GoI interpretation of linear logic proofs. We then complete our journey by going back from type-free GoI-models to discover that we arrive at models of untyped combinatory logic.