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.
Programme
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 HofmannMislove Theorem
17.00 Short Break
17.15 Jan Rutten Exercises in coalgebra – a coinductive proof of Moessner's theorem
18.00 Close.
Abstracts
Anchor  


Edmund Robinson
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.
Anchor  


Peter Mosses
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: closedinstance
(ci) bisimilarity and formalhypothesis (fh) bisimilarity, both
due to De Simone (1) and hypothesispreserving (hp) bisimilarity,
due to Rensink (2).
We give simple examples showing that for cibisimilarity,
sound equations on open terms are not preserved by disjoint
extensions. For both fhbisimilarity and hpbisimilarity,
arbitrary sound equations on open terms are preserved
by all disjoint extensions which do not add labels. Moreover,
for slight variations of fh and hpbisimilarity, all sound
equations are preserved by arbitrary disjoint extensions.
See (3) for further details and proofs.
References:
(1) R. de Simone (1985): HigherLevel Synchronizing Devices
in MEIJESCCS. 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.
Anchor  


Ross Horne
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 semistructured 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 Hopfmodule 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.
Anchor  


Achim Jung
The HofmannMislove Theorem
The HofmannMislove Theorem states that there is a bijection
between Scottopen 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 fourvalued logic.
Anchor  


Jan Rutten
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).
Attendance
From Bath:
 Martin Churchill
 Pierre Clairambault
 Anupam Das
 Guy McCusker
 John Power
 Cai Wingfield
From Birmingham:
 Achim Jung
From Imperial:
 Faris AbouSaleh
 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 AubreyJones
From Swansea:
 Ulrich Berger
 Tie Hou
 Peter Mosses
 Monika Seisenberger
From CWI (Netherlands):
 Jan Rutten
From McGill (Canada):
 Prakash Panangaden