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 2008

OLD AND NEW PARADIGMS

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

• Friday 25 January (week 2) [Damien Woods] (UC Cork) The complexity of small universal Turing machines

• Friday 1 February (week 3) [Ian Horrocks] (OUCL) Description Logic Based Ontology Languages

• Friday 8 February (week 4) [Guy McCusker] (Bath) A games model of bunched implications

• Friday 22 February (week 6) [Rob Spekkens] (Cambridge) POSTPONED TILL NEXT TERM

• Friday 29 February (week 7) [Thorsten Altenkirch] (Nottingham) Is Intuitionistic Logic relevant for Computer Science?

• Friday 7 March (week 8) [Barry Cooper] (Leeds) How Computationally Relevant is Definability?

ABSTRACTS:

Damien Woods: We present some work concerned with small universal Turing machines, tag systems, and cellular automata. In particular we focus on program size and time complexity results.

For example, it has been an open question for some time as to whether the smallest known universal Turing machines of Minsky, Rogozhin, Baiocchi and Kudlek are efficient (polynomial time) simulators of Turing machines. Previously, the best known simulations were exponentially slow. We discuss recent work that shows that these machines are indeed efficient simulators. As a related result we also find thatRule 110, a well-known cellular automaton, is also efficiently universal. From the point of view of universal program-size we present new results on three variants of the the one tape Turing machine model: standard, semi-weak and weak. These machines are some of the most intuitively simple general purpose computational devices.

This is joint work with Turlough Neary.

Ian Horrocks: Description Logics (DLs) are a family of class based knowledge representation formalisms characterised by the use of various constructors to build complex classes from simpler ones, and by an emphasis on the provision of sound, complete and (empirically) tractable reasoning services. Although they have a range of applications (e.g., configuration and information integration), they are perhaps best known as the basis for widely used ontology languages such as OWL. The decision to base OWL on DLs was motivated by a requirement that key inference problems be decidable, and that it should be possible to provide "practical" reasoning services to support ontology design and deployment. This talk will introduce description logics and their relationship to OWL, and then describe some of the algorithms and implementation techniques that have enabled them to satisfy this requirement in spite of the discouraging worst case complexity of the relevant decision problems.

Guy McCusker: A game semantics of the implication-only fragment of O'Hearn and Pym's Logic of Bunched Implications (BI) is presented. The model is based on Hyland-Ong-style innocent strategies, augmented with new conditions to capture the resource control aspects of the logic. It is shown that the model has the property of full completeness; that is, every finite element of the model is the denotation of a proof of BI. This is joint work with David Pym (HP Labs, Bristol).

Thorsten Altenkirch: Modern Mathematics is based classical logic and Zermelo-Fraenkel set theory. In this talk I'll discuss why an intuitionistic approach, such as Martin-Loef's Type Theory, may be more appropriate for Computer Science.

Barry Cooper: A large part of the scientific enterprise is bringing plausible descriptions of reality within practical computational frameworks. Mathematically, it is easy to describe classically incomputable objects from algorithmic ingredients. And the technical links between definability and computability have been extensively mapped out. What is far from clear is the extent to which the hierarchies and fine-structure theories built from simple computational ingredients are mirrored in the material world. On the other hand, the recognition of the real-world computational content of definability does seem to offer a widely applicable explanatory potential.