The ninth meeting of the Wessex Theory Seminar will take place on Thursday 4th November 2010 at Imperial College London. Talks will be held in Room 343 of the Department of Computing, 180 Queen's Gate.

13.15 Edmund Robinson: Functional Interpretations and Proof Mining

13.45 Peter Mosses: On bisimulation and modularity

14.15 Coffee Break

14.45 Ross Horne: Linked Data Algebra

15.30 Coffee Break

16.00 Achim Jung: The Hofmann-Mislove Theorem

17.00 Short Break

17.15 Jan Rutten Exercises in coalgebra – a coinductive proof of Moessner's theorem

18.00 Close.

**Functional Interpretations and Proof Mining**

Goedel's Dialectica interpretation has recently gained new life as a

way of getting constructive information from classical proofs. This talk

gives an introduction to the transformation, describes some previous work

due to Oliva and Kohlenbach and introduces some new work of Oliva and Powell.

It concludes with a recap on the structure of the transformation from a more

semantic perspective.

**On bisimulation and modularity**

Sound behavioral equations on open terms may become unsound after

conservative extensions of the underlying operational semantics.

Providing criteria under which such equations are preserved is

extremely useful; in particular, it can avoid the need to repeat

proofs when extending the specified language.

In this talk we consider preservation of sound equations for

several notions of bisimilarity on open terms: closed-instance

(ci-) bisimilarity and formal-hypothesis (fh-) bisimilarity, both

due to De Simone (1) and hypothesis-preserving (hp-) bisimilarity,

due to Rensink (2).

We give simple examples showing that for ci-bisimilarity,

sound equations on open terms are not preserved by disjoint

extensions. For both fh-bisimilarity and hp-bisimilarity,

arbitrary sound equations on open terms are preserved

by all disjoint extensions which do not add labels. Moreover,

for slight variations of fh- and hp-bisimilarity, all sound

equations are preserved by arbitrary disjoint extensions.

See (3) for further details and proofs.

References:

(1) R. de Simone (1985): Higher-Level Synchronizing Devices

in MEIJE-SCCS. Theoretical Computer Science 37, pp. 245¿Äì267.

(2) A. Rensink (2000): Bisimilarity of Open Terms.

Information and Computation 156, pp. 345¿Äì385.

(3) P. D. Mosses, M. R. Mousavi & M. A. Reniers (2010):

Robustness of Equations Under Operational Extensions.

Proc. EXPRESS 2010. EPTCS, to appear; preliminary version

available.

**Linked Data Algebra**

On the 15th October 2010 the first specification of SPARQL

Update with anopertional semantics was published by the W3C.

SPARQL Update is a proposed language for updating RDF, where

RDF is the semi-structured data format of the project to establish

a Web of Linked Data.

Independently, I have been working on an operational semantics

for SPARQL Update. The operational semantics are expressed in terms

of a new process calculus, called the syndication calculus. Surprisingly,

the process calculus turns out to resemble a fragment of Linear Logic.

This is due to the resource sensitivity and synchronisation primitives

required to control updates. Furthermore, bisimulation derives an algebra

over updates, which establishes a verified basis for optimisations. The

algebraic properties established lead to speculation that the setting for

programming Linked Data is a calculus which covers a larger fragment of

Linear Logic and is sound with respect to some Hopf-module over a quantale.

I conclude by reflecting on the value of such interactions between the

intuition of an engineering problem and the foundations of programming languages.

**The Hofmann-Mislove Theorem**

The Hofmann-Mislove Theorem states that there is a bijection

between Scott-open filters of open sets and compact saturated subsets of

a sober space. What is to all appearances a technical result from Stone

duality has over the years been found to play a central role in

mathematical semantics. In this talk I plan to give an introduction to

the theorem, its setting, its proof, its applications, and a more recent

generalisation to four-valued logic.

**Exercises in coalgebra – a coinductive proof of Moessner's theorem**

Coinduction has come to play an ever more important role in

theoretical computer science, for the specification of and reasoning about

infinite data structures and, more generally, automata with infinite behaviour.

In this talk, we shall focus on a recently introduced formalism

for coinductive definitions: behavioural differential equations,

with which one specifies behaviour in terms of initial outputs and

behavioural derivatives (next state operators). Our emphasis will be on

the elementary calculus of streams (infinite sequences), of which we shall

discuss the basic theory, developed in close analogy to

mathematical analysis.

As an application area, we will discuss a coinductive calculus

of periodic stream operators. Using this calculus, we will give a new

and transparent proof of Moessner's theorem (1951) using coinduction.

This theorem gives a suprising construction for the stream of powers

n^k of the natural numbers (such as 1,8,27,64, ... for k=3) out of

the stream of natural numbers by an alternating process of

stream sampling and taking partial sums.

This is joint work with Milad Niqui (CWI).

From Bath:

- Martin Churchill
- Pierre Clairambault
- Anupam Das
- Guy McCusker
- John Power
- Cai Wingfield

From Birmingham:

- Achim Jung

From Imperial:

- Faris Abou-Saleh
- Nick Bezhanishvili
- Fredrik Dahlqvist
- Andrew V. Jones
- Clemens Kupke
- Björn Lellmann
- Dirk Pattinson
- Florian Widmann

From Queen Mary:

- Paulo Oliva
- Edmund Robinson
- Tom Powell
- Dan Hernest
- Rob Arthan

From Southampton:

- Gabrielle Anderson
- Ross Horne
- Corina Cirstea
- Toby Wilkinson
- Tristan Aubrey-Jones

From Swansea:

- Ulrich Berger
- Tie Hou
- Peter Mosses
- Monika Seisenberger

From CWI (Netherlands):

- Jan Rutten

From McGill (Canada):

- Prakash Panangaden