We present the first complete soundness proof of the anti-frame rule, a recently proposed proof rule for capturing information hiding in the presence of higher-order store. Our proof involves solving a non-trivial recursive domain equation, and it helps identify some of the key ingredients for soundness.
Full version with proofs available from Hongseok's homepage.
Download PDF Show BibTeX
Login to edit
Wed Sep 16 10:47:00 2009