The Oxford Advanced Seminar on Informatic Structures

Introduction to OASIS

Michaelmas 2004

Hilary 2005

Trinity 2005

Michaelmas 2005

Hilary 2006

Trinity 2006

Michaelmas 2006

Hilary 2007

Trinity 2007

Michaelmas 2007

Hilary 2008

Trinity 2008

Hilary 2007

MODELS OF REALITY

Talks are Friday afternoons at 2:00pm in the NEW Lecture Theatre of the Computing Laboratory. The Computing Laboratory is located at the corner of Parks road and Keble road. Abstracts can be found at the bottom of this page. Everyone is welcome!

• Friday 26 January (week 2) [Misha Gavrilovich] (Humboldt Universitat Berlin - Mathematics) A categoricity property of the Poincare fundamental groupoid functor

• Friday 2 February (week 3) [Maribel Fernandez] (King's College London - Computing) The Power of Closed Reduction

• Friday 9 February (week 4) [Hannes Leitgeb] (Bristol - Philosophy) Networks and Conditional Reasoning

• Friday 23 February (week 6) [Ross Duncan] (OUCL) Types for Quantum Computing

• Friday 2 March (week 7; 4PM) [Joachim Lataillade] (PPS - Paris 7) Second-order Game Semantics and Type Isomorphisms

• Friday 9 March (week 8) [Vladimiro Sassone] (Southampton - Computing) TBA

• Friday ? (week ?) [Basil Hiley] (Birkbeck College London - Physics) Basil will be giving his intended plenary [CKC]-talk which had to be postponed due to illness

ABSTRACTS:

Misha Gavrilovich: I will try to argue that model theoretic critetia may be useful in the analysis of the structures apprearing in category theory, and that, in particular, somtimes the model-theoretic notion of categoricity can be phrased in the language of category theory. I will do so on the example of the Poincare fundamental groupoid functor : the model theoretic analyis leads to conjecture a uniqueness (universality) property of this functor considered on a subcategory of the category of algebraic varieties; the techniques of model theory allow us to prove the result by reducing it to several facts of algebraic geometry.

Maribel Fernandez: Closed reduction strategies in the lambda-calculus restrict the reduction rules: the idea is that reductions may only take place when certain terms are closed (i.e. do not contain free variables). This has lead to various applications, such as an alpha-conversion free calculus of explicit substitutions, and an efficient abstract machine. In this talk I will describe a new application of this strategy to a linear version of Goedel's System T. We will show that a linear System T with closed reduction offers a huge increase in expressive power over the usual linear systems, which are `closed by construction' rather than `closed at reduction'.

Hannes Leitgeb: We will deal with the (i) representation of conditionals in neural-like networks and with the question (ii) how such networks are able to reason on the basis of these representations. One can prove that if the representation of conditionals in networks is "distributed", each of the systems of nonmonotonic logic in Kraus, Lehmann, and Magidor (1990) turns out to be adequate with respect to a particular network semantics. We will interpret this result in the context of the debate on "symbolic vs. distributed representation", we will investigate which properties of the world, if any, are tracked by such conditional representations in networks, and we will end up with an open question about possible extensions of these results to learning networks and their description in terms of systems of inductive logic.

Ross Duncan: Quantum computation is a novel computational paradigm which makes use of entanglement -- non-local correlations -- to perform computations. From a mathematical point of view, a pair of entanged entangled systems may be viewed as a physical realistion of the linear function type -- or more precisely as the PAR connective of multiplicative linear logic (MLL). In this talk I will examine the possibilities and limitations of linear logic as a typing regime for quantum processes, and how those limitations may be overcome using a generalised logical system based on polycategories.

Joachim de Lataillade: Thanks to its precision and its simplicity, game semantic can be a powerful tool for analysing syntax. This is the case in particular for type isomorphisms, which can be efficiently captured by game models. I will present a game model of polymorphic lambda-calculus (system F), inspired by preceding works on the subject, and explain how it can be applied first to retrieve Church-style type isomorphisms, and then to give a new, complete characterisation of Curry-style ones. The question of parametricity in this context will be introduced as a perspective.