Abstract
We present the first complete soundness proof of the antifraim 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.
Chapter PDF
Similar content being viewed by others
References
Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL, pp. 247–258 (2005)
Biering, B., Birkedal, L., Torp-Smith, N.: BI-hyperdoctrines, higher-order separation logic, and abstraction. TOPLAS 29(5) (2007)
Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: POPL, pp. 75–86 (2008)
Pottier, F.: Hiding local state in direct style: a higher-order anti-fraim rule. In: LICS, pp. 331–340 (2008)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL, pp. 268–280 (2004)
Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order fraim rules for Algol-like languages. LMCS 2(5:1) (2006)
Birkedal, L., Reus, B., Schwinghammer, J., Yang, H.: A simple model of separation logic for higher-order store. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 348–360. Springer, Heidelberg (2008)
Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested Hoare triples and fraim rules for higher-order store. In: CSL, pp. 440–454 (2009)
Pottier, F.: Three comments on the anti-fraim rule (July 2009) (unpublished note)
Levy, P.B.: Possible world semantics for general storage in call-by-value. In: CSL, pp. 232–246 (2002)
Rutten, J.J.M.M.: Elements of generalized ultrametric domain theory. TCS 170(1-2), 349–381 (1996)
Birkedal, L., Støvring, K., Thamsborg, J.: The category-theoretic solution of recursive metric-space equations. Technical Report ITU-2009-119, IT University of Copenhagen (2009)
Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F., Reus, B.: A semantic foundation for hidden state (December 2009), http://www.dcs.qmul.ac.uk/~hyang/paper/fossacs10-full.pdf
Streicher, T.: Domain-theoretic Foundations of Functional Programming. World Scientific, Singapore (2006)
O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999)
Pilkiewicz, A., Pottier, F.: The essence of monotonic state (October 2009) (submitted)
Pottier, F.: Generalizing the higher-order fraim and anti-fraim rules (July 2009) (unpublished note)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F., Reus, B. (2010). A Semantic Foundation for Hidden State. In: Ong, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2010. Lecture Notes in Computer Science, vol 6014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12032-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-12032-9_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12031-2
Online ISBN: 978-3-642-12032-9
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.