Publication details

Saarland University Computer Science

A Semantic Foundation for Hidden State

Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, Bernhard Reus

Foundations of Software Science and Computation Structures (FOSSACS 2010), Vol. 6014 of Lecture Notes in Computer Science, pp. 2-16, Springer, March 2010

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

Webmaster, Wed Sep 16 10:47:00 2009