A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces

  • Jan Schwinghammer
  • Lars Birkedal
  • Kristian St ø vring
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6604)

Abstract

Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow one to hide irrelevant parts of the state during verification, whereas the anti-frame rule allows one to hide local state from the context. We give the first sound model for Charguéraud and Pottier’s type and capability system including both frame and anti-frame rules. The model is a possible worlds model based on the operational semantics and step-indexed heap relations, and the worlds are constructed as a recursively defined predicate on a recursively defined metric space.

We also extend the model to account for Pottier’s generalized frame and anti-frame rules, where invariants are generalized to families of invariants indexed over pre-orders. This generalization enables reasoning about some well-bracketed as well as (locally) monotonic uses of local state.

References

  1. 1.
    Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: POPL (2009)Google Scholar
  2. 2.
    Ahmed, A., Fluet, M., Morrisett, G.: L3: A linear language with locations. Fundam. Inf. 77(4), 397–449 (2007)MATHGoogle Scholar
  3. 3.
    America, P., Rutten, J.J.M.M.: Solving reflexive domain equations in a category of complete metric spaces. J. Comput. Syst. Sci. 39(3), 343–375 (1989)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Biering, B., Birkedal, L., Torp-Smith, N.: BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst. 29(5) (2007)CrossRefGoogle Scholar
  5. 5.
    Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules for Algol-like languages. LMCS 2(5:1) (2006)Google Scholar
  6. 6.
    Birkedal, L., Reus, B., Schwinghammer, J., Støvring, K., Thamsborg, J., Yang, H.: Step-indexed Kripke models over recursive worlds. In: POPL (to appear, 2011)Google Scholar
  7. 7.
    Birkedal, L., Støvring, K., Thamsborg, J.: Realizability semantics of parametric polymorphism, general references, and recursive types. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 456–470. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  8. 8.
    Charguéraud, A., Pottier, F.: Functional translation of a calculus of capabilities. In: Proceedings of ICFP, pp. 213–224 (2008)Google Scholar
  9. 9.
    Crary, K., Walker, D., Morrisett, G.: Typed memory management in a calculus of capabilities. In: Proceedings of POPL, pp. 262–275 (1999)Google Scholar
  10. 10.
    Dreyer, D., Neis, G., Birkedal, L.: The impact of higher-order state and control effects on local relational reasoning. In: Proceedings of ICFP (2010)Google Scholar
  11. 11.
    Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)MATHGoogle Scholar
  12. 12.
    Pilkiewicz, A., Pottier, F.: The essence of monotonic state (July 2010) (unpublished)Google Scholar
  13. 13.
    Pitts, A.M.: Relational properties of domains. Inf. Comput. 127(2), 66–90 (1996)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Pottier, F.: Hiding local state in direct style: a higher-order anti-frame rule. In: Proceedings of LICS, pp. 331–340 (2008)Google Scholar
  15. 15.
    Pottier, F.: Generalizing the higher-order frame and anti-frame rules (July 2009) (unpublished), http://gallium.inria.fr/~fpottier
  16. 16.
    Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested hoare triples and frame rules for higher-order store. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 440–454. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  17. 17.
    Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F., Reus, B.: A semantic foundation for hidden state. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 2–17. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  18. 18.
    Smyth, M.B.: Topology. In: Handbook of Logic in Computer Science, vol. 1. Oxford Univ. Press, Oxford (1992)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Jan Schwinghammer
    • 1
  • Lars Birkedal
    • 2
  • Kristian St ø vring
    • 3
  1. 1.Saarland UniversityGermany
  2. 2.ITUniversity of CopenhagenDenmark
  3. 3.DIKUUniversity of CopenhagenDenmark

Personalised recommendations