Venue

Electronic Notes on Theoretical Computer Science, vol. 172, pp. 133–175

Publication Year

2007

Authors

Abstract

We present local Hoare reasoning about data update, using Context Logic for analysing structured data. We apply our reasoning to tree update, heap update which is analogous to local Hoare reasoning using Separation Logic, and term rewriting.

Source Materials