A Semantic Foundation for Hidden State

Abstract. We present the first complete soundness proof of the antiframe 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.

• Type: Conference
• Year: 2010
• Where: FOSSACS
• Authors: Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, Bernhard Reus
• Keywords: Applied Computing, Complete Soundness Proof, FOSSACS 2010, Proof Rule, Recursive Domain Equation