The sixth meeting of the Wessex Theory Seminar returned to Southampton on Friday 19th February 2010. Talks took place in the seminar room on the 4th floor, Mountbatten building, Highfield campus, Southampton University. The event was fully catered with lunch and coffee.
10:15-10:45 Welcome coffee
10:45-11:30 Paulo Oliva: Selection Functions in Proof Theory .
11:30-12:30 Max Kanovich: How and Why Purely Propositional Separation Logic is undecidable .
1:30-2:15 Dirk Pattinson: Global Caching for Coalgebraic Description Logics .
2:15-2:50 Mark Wheelhouse: High Level Program Reasoning .
2:50-3:15 Afternoon tea
3:15-4:15 Andrzej Murawski: Full Abstraction for Reduced ML .
4:15-5:00 Kohei Honda: The pi-calculus in the Real World .
From Queen Mary:
Selection Functions in Proof Theory
By "selection function" we mean an operation that selects a witness to the non-emptyness
of any given property/set (if that property/set is indeed 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)
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 connectives, the most important feature of
separation logic is its separating 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 for h2.
Here our main focus is on the logic for concrete heap-like
models of practical interest.
Via an encoding of Minsky machines, we show that:
On top of that, our undecidability results for concrete heap-like
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 decidability.
E.g., we can deduce that to obtain decidability in a heap-like
model, one should either give up infinite interpretations for
atomic propositions (as in Calcagno-Yang-O'Hearn) or restrict
the formula language (as in Berdine-Calcagno-O'Hearn).
We prove undecidability for a number of natural propositional
systems developed on the road towards axiomatization of
separation logic, such as
Notice that adding the unrestricted *-weakening to Boolean BI
(as well as to Classical BI) forces a collapse into the standard
Boolean logic, 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 adjoint implications, respectively.
(Neither negation nor `false' should be blamed for its undecidability)
(See also http://www.doc.ic.ac.uk/research/technicalreports/2010/)
This is joint work with James Brotherston (Imperial)
Global Caching for Coalgebraic Description Logics
Coalgebraic description logics offer a common semantic umbrella for extensions of description logics with reasoning principles outside relational semantics, e.g. quantitative uncertainty, non-monotonic conditionals, or coalitional power. Specifically, we work in coalgebraic logic with global assumptions (i.e. a general TBox), nominals, and satisfaction operators, and prove soundness and completeness of an associated tableau algorithm of optimal complexity EXPTIME. The algorithm is based on global caching, which raises hopes of practically feasible implementation. Instantiation of this result to concrete logics yields new algorithms in all cases including standard relational hybrid logic.
This is joint work with Rajeev Gore (ANU), Clemens Kupke (Imperial) and Lutz Schroeder (DFKI Bremen).
High Level Program Reasoning
O'Hearn, Reynolds and Yang introduced Separation Logic to provide modular reasoning about simple,
mutable data structures in memory. They were able to construct small specifications of programs by
reasoning about the local parts of memory accessed by programs (their footprints). They have used
their Low-Level reasoning to notable success verifying memory safety properties of C programs and
Gardener, Calcagno and Zarfaty have generalised this work, introducing Context Logic to reason about
more complex, High-Level, data structures in order to reason at the level of the program abstraction.
In particular, with Smith and Wheelhouse, they have developed a formal, compositional specification
for the Document Object Model (DOM) a W3C XML update library. However, whilst keeping to the spirit
of local reasoning, they were not able to retain small specifications for all of their update commands.
We have since introduced Segment Logic, which provides a more fine-grained 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 verification from Low-Lewel to
High-Level reasoning. We will begin with a quick look at Separation Logic before introducing Context
Logic and showing how this enables us to specify the High-Level DOM commands without needing to
know how they are implemented at the Low-Level. We shall then see how these specifications are
unsuitable for reasoning about a concurrent XML update language, and look at how Segment Logic
can be used to provide a more fine-grained specification of these commands that can be used in a
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
information 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.
The pi-calculus in the Real World
Along with technical stuff, I hope I can discuss why my industry colleagues have come to like types, logics and bisimulations.