Local Resource Reasoning about Program Modules such as DOM
In this talk, I will describe recent work on fine-grained reasoning about program modules, using the W3C XML update library
DOM as the running example. In particular, I will present an axiomatic specification of DOM using Context Logic, and verify
DOM implementations by introducing locality-preserving and locality-breaking translations between the abstract DOM specification
and the concrete implementations.