MATH 670. Linear Logic and Game Semantics
(3 hours of lecture per week).
Linear logic was invented by Girard in 1987 and was originally motivated by an investigation of the semantics of $\lambda$-calculus. Since its invention it has had tremendous impact on mathematical logic and theoretical computer science, with applications in logic programming, language design, formal verification and semantics, to name a few. It has brought along new ways of analyzing the structure of logical rules in a search for a deeper understanding of their meaning. Currently there are several research centers around the world, both industry and academy, concentrating on research on several aspects and applications of linear logic.
In recent years there has been a paradigm shift in the field of mathematical theory of programming, from modelling computation to modelling interaction. This reflects the shift in information technology from stand alone computers and programs to networks and systems. The Internet being a vivid example. One very successful approach in this new framework has been the game semantics. It has a fairly long history in logic, going back to Lorenzen in the 50's. Major contributions were later made by Joyal (1977) who organised Conway games into a category and Blass (1992) who gave a semantics for linear logic. Later on the work of Abramsky, Hyland, Jagadeesan, Nickau and Ong among others has added a lot of interesting material to this field. In particular, a long standing open problem, namely the full abstraction problem for the language PCF was settled independently by Abramsky, Jagadeesan and Malacaria; Hyland and Ong; and Nickau using game semantics.
In this course we plan to give a thorough introduction to linear logic and its models, in particular categorical models that connect the models of linear logic to categories of particular importance in other branches of mathematics and theoretical physics (monoidal, compact closed and traced categories). We will briefly discuss the ideas behind the Geometry of Interaction, a new form of semantics which can be placed in the middle ground between the extant denotational and operational semantics and will mention the relevance of operator theoretical methods to certain models for geometry of interaction. We will also spend a considerable part of the course discussing the game semantics for linear logic. In particular, we will study game models introduced and studied by Abramsky and Jagadeesan, and Hyland and Ong. The relevance of such models to computer Science applications will be emphasized. In particular, we will discuss the full abstraction problem for PCF (Programming language for Computable Functions).
A tentative schedule appears below:
Go to: | MATH 670 | Course Information | Course Material | News |