Publication details
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
@PROCEEDINGS{SchwinghammerEtAl:2010:A-Semantic,
title = {A Semantic Foundation for Hidden State},
author = {Jan Schwinghammer and Hongseok Yang and Lars Birkedal and François Pottier and Bernhard Reus},
year = {2010},
month = {Mar},
editor = {C.-H. L. Ong},
publisher = {Springer},
booktitle = {Foundations of Software Science and Computation Structures (FOSSACS 2010)},
series = {Lecture Notes in Computer Science},
volume = {6014},
pages = {2-16},
}
Login to edit
Legal notice, Privacy policy
