There has been a recent breakthrough in Hoare reasoning. Researchers previously used Hoare reasoning based on First-order Logic to specify how programs interacted with the whole memory. O'Hearn, Reynolds and Yang instead introduced local Hoare reasoning based on Separation Logic. The key idea is to specify how programs interact with the small, local part of the memory (the footprint) touched by a program. Their work is proving to be essential for modular reasoning about large programs, and for reasoning about modern applications involving concurrent, distributed programming.
Inspired by this work, Calcagno, Gardner and Zarfaty studied local Hoare reasoning about XML update. We initially assumed that we could base our reasoning on Cardelli and Gordon's Ambient Logic, which analyses static trees (firewalls, XML) in a similar way to O'Hearn's analysis of heaps. In fact, we proved that this is not possible. Instead, we had to fundamentally change the way we reason about structured data, by introducing Context Logic for reasoning about both data and contexts.
In this talk, I will give an overview of local Hoare reasoning about XML update, based on Context Logic. This talk will be aimed at a general audience. I gather that Peter O'Hearn has recently given a talk on a verification tool based on Separation Logic. I will not assume knowledge of Separation Logic, but I hope that you will understand the connections between our work from my talk.
Dr Philippa Gardner
Philippa Gardner is a Reader at Imperial College, and holds a five-year senior research fellowship sponsored by Microsoft Research Cambridge and the Royal Academy of Engineering. Her current research spans programming language design, process models and web languages. She completed her Ph.D at Edinburgh in 1992 on type theory and logical frameworks, supervised by Gordon Plotkin, and has held several additional fellowships,including an EPSRC Advanced Fellowship at Cambridge University and Imperial College.