A. Ahmed, D. Dreyer, and A. Rossberg, State-dependent representation independence, Proceedings of POPL, pp.340-353, 2009.
DOI : 10.1145/1480881.1480925

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

P. America and J. J. Rutten, Solving reflexive domain equations in a category of complete metric spaces, Journal of Computer and System Sciences, vol.39, issue.3, pp.343-375, 1989.
DOI : 10.1016/0022-0000(89)90027-5

A. W. Appel and D. A. Mcallester, An indexed model of recursive types for foundational proof-carrying code, ACM Transactions on Programming Languages and Systems, vol.23, issue.5, pp.657-683, 2001.
DOI : 10.1145/504709.504712

L. Benton, A. Birkedal, C. Kennedy, and . Varming, Formalizing domains, ultrametric spaces and semantics of programming languages, 2010.

B. Biering, L. Birkedal, and N. Torp-smith, BI-hyperdoctrines, higher-order separation logic, and abstraction, ACM Transactions on Programming Languages and Systems, vol.29, issue.5, 2007.
DOI : 10.1145/1275497.1275499

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

L. Birkedal, B. Reus, J. Schwinghammer, K. Støvring, J. Thamsborg et al., Stepindexed Kripke models over recursive worlds, Proceedings of POPL, pp.119-132, 2011.

L. Birkedal, B. Reus, J. Schwinghammer, and H. Yang, A Simple Model of Separation Logic for Higher-Order Store, Proceedings of ICALP, pp.348-360, 2008.
DOI : 10.1007/978-3-540-70583-3_29

L. Birkedal, K. Støvring, and J. Thamsborg, Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types, Proceedings of FOSSACS, pp.456-470, 2009.
DOI : 10.1137/0211062

L. Birkedal, K. Støvring, and J. Thamsborg, The category-theoretic solution of recursive metric-space equations, Theoretical Computer Science, vol.411, issue.47, pp.4102-4122, 2010.
DOI : 10.1016/j.tcs.2010.07.010

L. Birkedal, N. Torp-smith, and H. Yang, Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages, Logical Methods in Computer Science, vol.2, issue.5, 2006.
DOI : 10.2168/LMCS-2(5:1)2006

A. Charguéraud and F. Pottier, Functional translation of a calculus of capabilities, Proceedings of ICFP, pp.213-224, 2008.

D. Dreyer, G. Neis, and L. Birkedal, The impact of higher-order state and control effects on local relational reasoning, Proceedings of ICFP, 2010.

A. Gotsman, J. Berdine, B. Cook, N. Rinetzky, and M. Sagiv, Local Reasoning for Storable Locks and Threads, 2007.
DOI : 10.1007/978-3-540-76637-7_3

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

A. Hobor, A. W. Appel, and F. Z. Nardelli, Oracle Semantics for Concurrent Separation Logic, Proceedings of ESOP, pp.353-367, 2008.
DOI : 10.1007/978-3-540-78739-6_27

P. B. Levy, Possible World Semantics for General Storage in Call-By-Value, Proceedings of CSL, pp.232-246, 2002.
DOI : 10.1007/3-540-45793-3_16

A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal, Abstract Predicates and Mutable ADTs in Hoare Type Theory, Proceedings of ESOP, pp.189-204, 2007.
DOI : 10.1007/978-3-540-71316-6_14

P. W. O-'hearn, Resources, concurrency and local reasoning, Theor. Comput. Sci, vol.375, issue.13, pp.271-307, 2007.

P. W. O-'hearn, H. Yang, and J. C. Reynolds, Separation and information hiding, Proceedings of POPL, pp.268-280, 2004.

M. Parkinson and G. Bierman, Separation logic and abstraction, Proceedings of POPL, pp.247-258, 2005.
DOI : 10.1145/1040305.1040326

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

M. Parkinson and G. Bierman, Separation logic, abstraction and inheritance, Proceedings of POPL, pp.75-86, 2008.
DOI : 10.1145/1328438.1328451

B. C. Pierce, Types and Programming Languages, 2002.

A. Pilkiewicz and F. Pottier, The essence of monotonic state, Proceedings of the 7th ACM SIGPLAN workshop on Types in language design and implementation, TLDI '11, pp.73-86, 2011.
DOI : 10.1145/1929553.1929565

URL : https://hal.archives-ouvertes.fr/hal-01081193

A. M. Pitts, Relational Properties of Domains, Information and Computation, vol.127, issue.2, pp.66-90, 1996.
DOI : 10.1006/inco.1996.0052

F. Pottier, Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.331-340, 2008.
DOI : 10.1109/LICS.2008.16

F. Pottier, Generalizing the higher-order frame and anti-frame rules. Unpublished note, 2009.

F. Pottier, Three comments on the anti-frame rule. Unpublished note, 2009.

F. Pottier, Syntactic soundness proof of a type-and-capability system with hidden state, Journal of Functional Programming, vol.4, issue.01, 2011.
DOI : 10.1016/j.scico.2006.02.003

URL : https://hal.archives-ouvertes.fr/hal-00877589

D. J. Pym, P. W. O-'hearn, and H. Yang, Possible worlds and resources: the semantics of BI, Theoretical Computer Science, vol.315, issue.1, pp.257-305, 2004.
DOI : 10.1016/j.tcs.2003.11.020

J. C. Reynolds, Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp.55-74, 2002.
DOI : 10.1109/LICS.2002.1029817

J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang, Nested Hoare Triples and Frame Rules for Higher-Order Store, Proceedings of CSL, pp.440-454, 2009.
DOI : 10.1142/6284

URL : http://arxiv.org/abs/1109.3031

J. Schwinghammer, L. Birkedal, and K. Støvring, A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces, Proceedings of FOSSACS, pp.305-319, 2011.
DOI : 10.1007/978-3-642-19805-2_21

J. Schwinghammer, H. Yang, L. Birkedal, F. Pottier, and B. Reus, A Semantic Foundation for Hidden State, Proceedings of FOSSACS, pp.2-16, 2010.
DOI : 10.1007/978-3-642-12032-9_2

F. Smith, G. Walker, and . Morrisett, Alias Types, Proceedings of ESOP, volume 1782 of Lecture Notes in Computer Science, pp.366-381, 2000.
DOI : 10.1007/3-540-46425-5_24

A. K. Wright, Simple imperative polymorphism, Lisp and Symbolic Computation, pp.343-356, 1995.
DOI : 10.1007/BF01018828

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=