Spatial Logic ATutorial Introduction
Stc
ComputingScienceColloquium
Date: June 26
Time: 11am
Room: C008 AARD
Speaker: Dave Clarke
Title: Spatial Logic: A Tutorial Introduction
Slides available http://www.cs.uu.nl/~dave/talks/spatiallogic.pdf
Abstract
Not only hot but also cool is the emergent field of
spatial logic. Stemming from bizarre notions such
as substructural logic (e.g., linear logic), spatial
logics enable the description of things (pointer
programs, graphs, XML documents) in separate components
that may contain unbound names. These components
can then be joined together using the connectives
of the logic, potentially providing bindings for the
unbound names. Spatial logics enable, for example, the
reasoning about parts of a program containing dangling
pointers, which can then be joined using the connectives
of the logic giving the pointers something to point to
(Cool, hey?). It is expected that this will enable more
modular and local reasoning.
This talk will cover two spatial logics. Firstly, it
will cover O'Hearn, Reynolds and Pym's Logic of Bunched
Implications and its application to reasoning about
low-level pointer programs. Secondly, the talk will
review Cardelli, Gordon, Gardner and Ghelli's Spatial
Logics and their application to semi-structured data
(XML) processing.
If time permits, the talk will also give an overview of
other applications of spatial logic, including some
speculative ideas regarding object-oriented programming.
--
DaveClarke - 20 Jun 2003
