Title: On categorical models for the geometry of interaction (Part I) (PDF slides)
Abstract: In a series of 3 lectures I will be discussing a categorical approach to Girard's Geometry of Interaction (GoI) program. I will start by discussing Unique Decomposition Categories (UDCs) that are the main mathematical structures used in our categorical approach to GoI. I will emphasize the critical role played by the notion of categorical trace in this approach. Next, I will describe the joint work with S. Abramsky and P.J. Scott which draws on the main mathematical ingredients of GoI to construct a Linear Combinatory Algebra (a linear version of the good old combinatory algebra). I will discuss this in the context of UDCs and also in full generality. Finally, I will discuss my recent joint work with P.J. Scott exteding the earlier categorical approach to the setting of a partially traced category with an abstract orthogonality relation. During all lectures I will discuss directions for future work and describe some current research.
Title: Why is GoI relevant for implicit computational complexity? (PDF slides)
Title: Basic results on traced monoidal categories (PDF slides)
Abstract: We survey some basic results on traced monoidal categories, including the trace-fixpoint correspondence, the Int-construction, and the relation to knot theory.
Title: On categorical models for the geometry of interaction (Part II) (PDF slides)
Title: From asynchronous games to coherence spaces (PDF slides)
Title: Initial Algebra Semantics for Cyclic Sharing Structures (PDF slides)
Abstract: "Tree-like" structures -- trees involving cycles and sharing -- appear very often in logic and computer science. They are usually treated as graphs, because there do not seem to exist clear inductive structures. I propose a simple term syntax for cyclic sharing structures that admits structural induction and recursion principles. I show that the obtained syntax is directly usable in the functional language Haskell, as well as ordinary data structures such as lists and trees. To achieve this goal, I use categorical approach to initial algebra semantics in a presheaf category. I will also try to relate this with traced categorical models.
Title: Attribute Grammars and Categorical Semantics
Abstract: We give a new formulation of attribute grammars (AG for short) called monoidal AGs in traced symmetric monoidal categories. Monoidal AGs subsume existing domain-theoretic, graph-theoretic and relational formulations of AGs. Using a 2-categorical aspect of monoidal AGs, we also show that every monoidal AG is equivalent to a synthesised one when the underlying category is closed, and that there is a sound and complete translation from local dependency graphs to relational AGs.
Title: On categorical models for the geometry of interaction (Part III) (PDF slides)
Title: Building a (sort of) geometry of interaction from denotational semantics (PDF slides)
Abstract: The relationship between geometry of interaction (or "cut-as-trace") and denotational semantics (or "cut-as-composition") has been extensively studied by Abramsky, Haghverdi and Scott. Their analysis assumes a certain "notion" of geometry of interaction (a suitable categorical axiomatization of Girard's original proposal), from which it is shown how denotational models can be built. We are interested in the reverse procedure: given a denotational model, we investigate if and how it makes to define a "geometry of interaction" out of it. We shall present some very partial and very limited preliminary results in this direction, with the hope of receiving lots of interesting feedback from the other workshop participants :-)
Title: Functional Programming in Sublinear Space (PDF slides)
Abstract: We are studying how programming in sublinear space can be supported by specifically designed programming languages. Writing programs with sublinear space usage often requires one to use special implementation techniques for common tasks. For example, one cannot compose two functions directly, as there may not be enough space for the intermediate result, but must instead compute and recompute small parts of the intermediate result on demand. Since such techniques are sometimes hard to handle, we are aiming to design a programming language that makes such techniques transparent and allows one to write programs in a more natural way.
This talk will be about an approach to developing a functional programming language for sublinear space. The approach is based on modelling computation by interaction in the style of particle style Geometry of Interaction. Following a semantic approach, we derive a functional programming language from the closely-related Int-construction, which allows one to study interactive computation on the basis of a given functional language. The proposed functional language is formulated by means of a type system inspired by Barber & Plotkin's Dual Linear Logic and Baillot & Terui's Dual Light Affine Logic. In order to assess the intensional expressiveness of the language, we implement in the language Moeller-Neergaard & Mairson's algorithm for sublinear space iteration by computational amnesia.
Title: KBO Orientability (PDF slides)
Abstract: Knuth-Bendix orders (1970) are a method for proving termination of term rewrite systems, which is one of the oldest but most popular methods. In this talk, based on joint work with Harald Zankl and Aart Middeldorp, I present a finite characterization of termination by Knuth-Bendix orders.
Title: No counterexample interpretation of logic and Geometry of Interaction (PDF slides)
Abstract: No counterexample interpretation (NCI) is introduced by Kreisel as a kind of functional interpretation of logic. Tait has shown that NCI for PA corresponds to the initial version of Gentzen's consistency proof, stated in terms of game. I will explain NCI a la Tait, point out the similarity between NCI and the Geometry of Interaction and explore how one can exploit this similarity.
Title : On the Meaning of Algebraic Weights Given by the GoI (PDF slides)
Abstract : Geometry of Interaction being an almost denotational semantics, the weights of paths before and after reduction must have the same global meaning. Nevertheless, it is very difficult to extract this meaning from the algebraic description.
We will start by presenting a fundamental example of this issue in the case of lambda-calculus. By looking at the GoI of a Church Integer n, it is really simple to understand it purposes. Now if we look at the GoI of (n)n which reduces to n^n it is a lot more complex. This obfuscation is due to a huge compression of the number of paths, from 2(n^n +1) to 2(2+n(n-1)).
We will then present the GoI of Differential Interaction Nets and how one can extract a meaning from weights that could be used to study concurrent processes. We will show the main steps needed to develop such a tool, and revive an idea from Girard: variants.
Title: Towards Geometry of Interaction for Hughes-vanGlabbeek Proof-Nets
Abstract: We study a geometry of interaction interpretation of Hughes-vanGlabbeek's MALL proof-nets. In the original style of GoI with partial isometries in operator algebra, we investigate a dynamic meaning of H-vG's criterion for switching cycles on top of Girard's execution formula.
Title: Int Construction and Semibiproduct
Abstract: We study a relationship between the Int construction and a weaking of biproducts called semibiproduct. Our main result is that Int construction is left biadjoint to the forgetful functor from the 2-category of compact closed categories with semibiproducts to the 2-category of traced distributive symmetric monoidal categories with biproducts. We give an example of a traced distributive symmetric monoidal category with biproducts and observe a relation between GoI interpretation of MALL.
Title: Ludics and Logical Completeness (PDF slides)
Title: From asynchronous games to coherence spaces (Contd.)