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
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
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.
(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
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
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 Queen Mary:
From CWI (Netherlands):
From McGill (Canada):