## Invited Speakers |
---|

- Jean-Yves
Girard (IML, Marseille).
**Title:**"Locus solum: from the rules of logic to the logic of rules" - Peter
O'Hearn (QMW College, London).
**Title:**"Local Reasoning about Programs that Alter Data Structures"

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

This paper 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"

**Abstract:**Many 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 - csl01@lsv.ens-cachan.fr