The sixth meeting of the Wessex Theory Seminar returned to South= ampton on Friday 19th February 2010. Talks took place in the seminar room o= n the 4th floor, Mountbatten building, Highfield campus, Southampton University.= The event was fully catered with lunch and coffee.

=2010:15-10:45 Welcome coffee

=20**Morning session**

10:45-11:30 Paulo Oliva: Se= lection Functions in Proof Theory .

=2011:30-12:30 Max Kanovich: How= and Why Purely Propositional Separation Logic is undecidable .

=2012:30-1:30 Lunch

=20**Afternoon session**

1:30-2:15 Dirk Pattinson: Gl= obal Caching for Coalgebraic Description Logics .

=202:15-2:50 Mark Wheelhouse: H= igh Level Program Reasoning .

=202:50-3:15 Afternoon tea

=20**Final session**

3:15-4:15 Andrzej Murawski: Full Abstraction for Reduced ML .

=204:15-5:00 Kohei Honda: The = pi-calculus in the Real World .

=20From Southampton:

=20- =20
- Julian Rathke =20
- Pawel Sobocinski =20
- Ross Horne =20
- Sardaouna Hamadou =20
- Corina Cirstea =20
- Issam Maamria =20
- Toby Wilkinson =20
- Gabrielle Anderson =20
- Ehab ElSalamouny =20
- Issam Souliah =20
- Tope Omitola =20

From Imperial:

=20- =20
- Dirk Pattinson =20
- Mark Wheelhouse =20
- James Brotherston =20
- Faris Abou-Saleh =20

From Queen Mary:

=20- =20
- Paulo Oliva =20
- Max Kanovich =20
- Kohei Honda =20
- Rob Arthan =20
- Gilda Ferreira =20

From Bath:

=20- =20
- Guy McCusker =20

From Oxford:

=20- =20
- Andrzej Murawski =20

From Swansea:

=20- =20
- Fredrik Nordvall Forsberg =20

=20

**Selection Functions in Proof Theory**

By "selection function" we mean an operation that selects a witness to t=
he non-emptyness

of any given property/set (if that property/set is ind=
eed non-empty). Hilbert's epsilon

terms provide one example of the=
role played by selection functions in proof theory. In this

talk =
I will show that, when generalised notions of predicate and quantifier are =
considered,

such selection functions have in fact a ubiquitous role in =
the computational interpretation

of proofs in arithmetic and analysis. =
(Joint work with Martin Escardo)

=20

**How and Why Purely Propositional Separation Logic is undecidable=
.**

*Separation logic* has proven as an adequate formalism for the

analysis of programs that manipulate memory (in the form of

pointers,=
heaps, stacks, etc.). In addition to the standard

propositional connec=
tives, the most important feature of

separation logic is its *separa=
ting conjunction* (A*B) which

holds for a heap h iff h can be split=
into *separate* h1

and h2 so that A holds for h1 and B holds fo=
r h2.

Here our main focus is on th=
e logic for *concrete* heap-like

models of practical inte=
rest.

Via an encoding of Minsky machines, we show that:

=20- =20
- It is undecidable whether a purely propositional formula A

is valid= in the class of all (total) separation models. =20
- It is undecidable whether a purely propositional formula A

is valid= in the class of all separation models with

indivisible units. =20
- Furthermore, whatever
*concrete*heap-like model H we take,

= it is undecidable whether a purely propositional formula A

is valid in = this model H. =20

On top of that, our undecidability results for *concrete* heap-li=
ke

models give new insights into the nature of decidable

fragments =
of separation logic such as those given by

Calcagno-Yang-O'Hearn(2001) =
and Berdine-Calcagno-O'Hearn(2004),

as well as imposing boundaries on d=
ecidability.

E.g., we can deduce that to obtain decidability in a heap-like

model=
, one should either give up infinite interpretations for

atomic proposi=
tions (as in Calcagno-Yang-O'Hearn) or restrict

the formula language (a=
s in Berdine-Calcagno-O'Hearn).

We prove undecidability for a number of natural propositional

system=
s developed on the road towards axiomatization of

separation logic, suc=
h as

- =20
- Boolean BI, =20
- Boolean BI enriched with a restricted *-weakening, =20
- Classical BI, =20
- Classical BI enriched with the restricted *-weakening. =20

Notice that adding the unrestricted *-weakening to Boolean BI

(as we=
ll as to Classical BI) forces a collapse into the standard

Boolean logi=
c, which is decidable.

To add a new exhibit to the Undecidability Zoo, we show

the simplest=
undecidable purely propositional system,

we call it Minimal BI, which =
employs only two conjunctions,

that is * and &, and their two adjoi=
nt implications, respectively.

(Neither negation nor `false' should be =
blamed for its undecidability)

(See also http://www.doc.ic.ac.uk/rese= arch/technicalreports/2010/)

=20This is joint work with James Brotherston (Imperial)

=20=20

**Global Caching for Coalgebraic Description Logics**

C=
oalgebraic description logics offer a common semantic umbrella for extensio=
ns of description logics with reasoning principles outside relational seman=
tics, e.g. quantitative uncertainty, non-monotonic conditionals, or coaliti=
onal power. Specifically, we work in coalgebraic logic with global assumpti=
ons (i.e. a general TBox), nominals, and satisfaction operators, and prove =
soundness and completeness of an associated tableau algorithm of optimal co=
mplexity EXPTIME. The algorithm is based on global caching, which raises ho=
pes of practically feasible implementation. Instantiation of this result to=
concrete logics yields new algorithms in all cases including standard rela=
tional hybrid logic.

This is joint work with Rajeev Gore (ANU), Clemens Kupke (Imperial) and = Lutz Schroeder (DFKI Bremen).

=20=20

**High Level Program Reasoning**

O'Hearn, Reynolds and Yang introduced Separation Logic to provide modula=
r reasoning about simple,

mutable data structures in memory. They were =
able to construct small specifications of programs by

reasoning about t=
he local parts of memory accessed by programs (their footprints). They have=
used

their Low-Level reasoning to notable success verifying memory saf=
ety properties of C programs and

device drivers.

Gardener, Calcagno and Zarfaty have generalised this work, introducing C=
ontext Logic to reason about

more complex, High-Level, data structures =
in order to reason at the level of the program abstraction.

In particul=
ar, with Smith and Wheelhouse, they have developed a formal, compositional =
specification

for the Document Object Model (DOM) a W3C XML update libr=
ary. However, whilst keeping to the spirit

of local reasoning, they wer=
e not able to retain small specifications for all of their update commands.=

We have since introduced Segment Logic, which provides a more fine-grain=
ed analysis of data structures

and yields small specifications for all =
of our update commands. As well as being aesthetically pleasing,

small =
specifications are essential for reasoning about concurrent update programs=
.

In this survey talk we shall take a look at the progression of program v=
erification from Low-Lewel to

High-Level reasoning. We will begin with =
a quick look at Separation Logic before introducing Context

Logic and s=
howing how this enables us to specify the High-Level DOM commands without n=
eeding to

know how they are implemented at the Low-Level. We shall then=
see how these specifications are

unsuitable for reasoning about a conc=
urrent XML update language, and look at how Segment Logic

can be used t=
o provide a more fine-grained specification of these commands that can be u=
sed in a

concurrent setting.

=20

**Full Abstraction for Reduced ML**

We present the first effectively presentable fully abstract model for

Stark's Reduced ML, the paradigmatic higher-order programming language

combining call-by-value evaluation and integer-valued references.

The model is constructed using techniques of nominal game semantics.

=
Its distinctive feature is the presence of carefully restricted

inform=
ation about the store in plays, combined with conditions

concerning the=
participants' ability to distinguish reference names.

This leads to an=
explicit characterization of program equivalence.

This is joint work with Nikos Tzevelekos.

=20=20

**The pi-calculus in the Real World**

Along with technical stuff, I hope I can discuss why my industry colleag= ues have come to like types, logics and bisimulations.