Girard (IML, Marseille). Title: "Locus solum: from the rules
of logic to the logic of rules"
O'Hearn (QMW College, London). Title: "Local Reasoning about
Programs that Alter Data Structures"
We describe an extension of Hoare's logic for reasoning about programs
that alter data structures. We consider a low-level storage model
based on a heap with associated lookup, update, allocation and
deallocation operations, and unrestricted address arithmetic. The
assertion language is based on a possible worlds model of the logic of
bunched implications, and includes spatial conjunction and implication
connectives alongside those of classical logic. Heap operations are
axiomatized using what we call the "small axioms", each of which
mentions only those cells accessed by a particular command. Through
these and a number of examples we show that the formalism supports
local reasoning: A specification and proof can concentrate on only
those cells in memory that a program accesses.
builds on earlier work by Burstall, Reynolds, Ishtiaq and O'Hearn on
reasoning about data structures.
- Jan Van den
Bussche (U. Limburg). Title: "Applications of Alfred
Tarski's Ideas in Database Theory"
ideas of Alfred Tarski---one of the founders of modern logic---find
application in database theory. We survey some of them with no attempt
at comprehensiveness. Topics discussed include the genericity of
database queries; the relational algebra, the Tarskian definition of
truth for the relational calculus, and cylindric algebras; relation
algebras and computationally complete query languages; real polynomial
constraint databases; and geometrical query languages.
- Peter F. Kenton (Bar of New York). Title: "Johnny's corner:
von Neumann seen by his cousin"
Last modified on 26th June 2001 - email@example.com