CS Talk
May 14, 2012
11:00 a.m., AKW 200

Speaker: Jules Villard, University College London
Title: The Ramify Rule of Separation Logic

Abstract: Separation logic provided a breakthrough in reasoning about the heap in many cases, making specs and proofs tractable and close to the programmer's intuition. Its "frame rule" enables local reasoning by answering the frame problem: describing what does not change when updating parts of the heap. However, for algorithms exhibiting intrinsic sharing, neither separation logic nor any other formalism has achieved simple proofs. We propose that most programs manipulating graphs, DAGs, or overlaid data structures require an answer to a different problem, the ramification problem (like the frame problem, another classic AI problem): describing how global structures change because of a local update. This work presents a solution in the form of a new inference rule: the ramify rule, mixing separation logic and relevant logic, and valid in any separation logic. We show how it allows sound and local reasoning about effects on data structures with sharing.

This is joint work with Aquinas Hobor from National University of Singapore.