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

=2013.15 Edmund Robinson: Fun= ctional Interpretations and Proof Mining

=2013.45 Peter Mosses: On bisi= mulation and modularity

=2014.15 Coffee Break

=2014.45 Ross Horne: Linked Dat= a Algebra

=2015.30 Coffee Break

=2016.00 Achim Jung: The Hofma= nn-Mislove Theorem

=2017.00 Short Break

=2017.15 Jan Rutten Exercises in= coalgebra =E2=80=93 a coinductive proof of Moessner's theorem

=2018.00 Close.

=20=20

**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 w=
ork

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

It concludes with a recap on the structure of the transfor=
mation from a more

semantic perspective.

=20

**On bisimulation and modularity**

Sound behavioral equations on open terms may become unsound after

co=
nservative extensions of the underlying operational semantics.

Providin=
g 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-) bisimilar=
ity 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 equa=
tions 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<=
br> equations are preserved by arbitrary disjoint extensions.

See (3) f=
or further details and proofs.

References:

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

in MEIJE=
-SCCS. Theoretical Computer Science 37, pp. 245=C2=BF=C3=84=C3=AC267.

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

Information and C=
omputation 156, pp. 345=C2=BF=C3=84=C3=AC385.

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

Robustne=
ss of Equations Under Operational Extensions.

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

available.

=20

**Linked Data Algebra**

On the 15th October 2010 the first specification of SPARQL

Update wi=
th anopertional semantics was published by the W3C.

SPARQL Update is a =
proposed language for updating RDF, where

RDF is the semi-structured da=
ta format of the project to establish

a Web of Linked Data.

Independently, I have been working on an operational semantics

for S=
PARQL Update. The operational semantics are expressed in terms

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

the p=
rocess calculus turns out to resemble a fragment of Linear Logic.

This =
is due to the resource sensitivity and synchronisation primitives

requi=
red to control updates. Furthermore, bisimulation derives an algebra

ov=
er updates, which establishes a verified basis for optimisations. The

a=
lgebraic 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 quanta=
le. I conclude by reflecting on the value of such interactions between =
the intuition of an engineering problem and the foundations of programm=
ing languages.**

=20

**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 sob=
er space. What is to all appearances a technical result from Stone

dual=
ity has over the years been found to play a central role in

mathematica=
l semantics. In this talk I plan to give an introduction to

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

generalis=
ation to four-valued logic.

=20

**Exercises in coalgebra =E2=80=93 a coinductive proof of Moessner=
's theorem**

Coinduction has come to play an ever more important role in

theoreti=
cal computer science, for the specification of and reasoning about

infi=
nite 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 de=
rivatives (next state operators). Our emphasis will be on

the elementar=
y calculus of streams (infinite sequences), of which we shall

discuss t=
he basic theory, developed in close analogy to

mathematical analysis.=20

As an application area, we will discuss a coinductive calculus

of pe=
riodic stream operators. Using this calculus, we will give a new

and tr=
ansparent proof of Moessner's theorem (1951) using coinduction.

This th=
eorem gives a suprising construction for the stream of powers

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

the stream =
of natural numbers by an alternating process of

stream sampling and tak=
ing partial sums.

This is joint work with Milad Niqui (CWI).

=20From Bath:

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

From Birmingham:

=20- =20
- Achim Jung =20

From Imperial:

=20- =20
- Faris Abou-Saleh =20
- Nick Bezhanishvili =20
- Fredrik Dahlqvist =20
- Andrew V. Jones =20
- Clemens Kupke =20
- Bj=C3=B6rn Lellmann =20
- Dirk Pattinson =20
- Florian Widmann =20

From Queen Mary:

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

From Southampton:

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

From Swansea:

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

From CWI (Netherlands):

=20- =20
- Jan Rutten =20

From McGill (Canada):

=20- =20
- Prakash Panangaden =20