Page History

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 Hofmann-Mislove Theorem

17.00 Short Break

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

18.00 Close.

Abstracts

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.

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: 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.

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 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.

Achim Jung

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.

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 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