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