. Abadi, . Martín, . Pierce, . Benjamin, and G. Plotkin, FAITHFUL IDEAL MODELS FOR RECURSIVE POLYMORPHIC TYPES, International Journal of Foundations of Computer Science, vol.02, issue.01, pp.1-21, 1991.
DOI : 10.1142/S0129054191000029

A. Ahmed, . Fluet, . Matthew, and G. Morrisett, L 3 : A linear language with locations, Fundamenta Informaticae, vol.77, issue.4, pp.397-449, 2007.

A. Ahmed, A. W. Appel, C. D. Richards, . Swadi, N. Kedar et al., Semantic foundations for typed assembly languages, ACM Transactions on Programming Languages and Systems, vol.32, issue.3, 2010.
DOI : 10.1145/1709093.1709094

A. J. Ahmed, . Fluet, . Matthew, and G. Morrisett, A step-indexed model of substructural state, Pages 78?91 of: ACM International Conference on Functional Programming (ICFP), 2005.

A. Ahmed and . Jamil, Semantics of types for mutable state, 2004.

P. Almeida and . Sérgio, Balloon types: Controlling sharing of state in data types, Pages 32?59 of: European Conference on Object-Oriented Programming, 1997.
DOI : 10.1007/BFb0053373

R. M. Amadio, . Cardelli, and . Luca, Subtyping recursive types, ACM Transactions on Programming Languages and Systems, vol.15, issue.4, pp.575-631, 1993.
DOI : 10.1145/155183.155231

URL : https://hal.archives-ouvertes.fr/inria-00070035

R. Atkey, Amortised resource analysis with separation logic, Pages 85?103 of: European Symposium on Programming (ESOP), 2010.

B. E. Aydemir, . Bohannon, . Aaron, . Fairbairn, . Matthew et al., Mechanized Metatheory for the Masses: The PoplMark Challenge, Pages 50?65 of: International Conference on Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science, 2005.
DOI : 10.1007/11541868_4

A. Barber, Dual intuitionistic linear logic, 1996.

C. J. Bell, . Dockins, . Robert, . Hobor, . Aquinas et al., Comparing semantic and syntactic methods in mechanized proof frameworks, International Workshop on Proof-Carrying Code (PCC), 2008.

K. Bierhoff and J. Aldrich, Modular typestate checking of aliased objects, Pages 301?320 of: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2007.

L. Birkedal, . Torp-smith, . Noah, 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

L. Birkedal, . Støvring, . Kristian, and J. Thamsborg, Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types, 2009.
DOI : 10.1137/0211062

L. Birkedal, . Støvring, . Kristian, and J. Thamsborg, Realisability semantics of parametric polymorphism, general references and recursive types, Mathematical Structures in Computer Science, vol.4960, issue.04, pp.655-703, 2010.
DOI : 10.1137/0211062

L. Birkedal, . Reus, . Bernhard, . Schwinghammer, . Jan et al., Step-indexed Kripke models over recursive worlds, Pages 119?132 of: ACM Symposium on Principles of Programming Languages (POPL), 2011.

F. Blanqui and A. Koprowski, CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, Mathematical Structures in Computer Science, vol.37, issue.04, pp.827-859, 2011.
DOI : 10.1016/S0890-5401(03)00011-7

URL : https://hal.archives-ouvertes.fr/inria-00543157

. Boyapati, . Chandrasekhar, . Lee, . Robert, and M. Rinard, Ownership types for safe programming: preventing data races and deadlocks, Pages 211?230 of: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2002.

J. Boyland and . Tang, Semantics of fractional permissions with nesting, ACM Transactions on Programming Languages and Systems, vol.32, issue.6, 2010.
DOI : 10.1145/1749608.1749611

J. Boyland, . Tang, and W. Retert, Connecting effects and uniqueness with adoption, Pages 283?295 of: ACM Symposium on Principles of Programming Languages (POPL), 2005.

M. Brandt and F. Henglein, Coinductive axiomatization of recursive type equality and subtyping, Fundamenta Informaticae, vol.33, pp.309-338, 1998.
DOI : 10.1007/3-540-62688-3_29

A. Buisse, L. Birkedal, and K. Støvring, Step-Indexed Kripke Model of Separation Logic for Storable Locks, Electronic Notes in Theoretical Computer Science, vol.276, pp.121-143, 2011.
DOI : 10.1016/j.entcs.2011.09.018

C. Calcagno, . O-'hearn, W. Peter, and H. Yang, Local Action and Abstract Separation Logic, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007.
DOI : 10.1109/LICS.2007.30

A. Charguéraud, The Locally Nameless Representation, Journal of Automated Reasoning, vol.40, issue.12, pp.363-408, 2012.
DOI : 10.1007/s10817-011-9225-2

A. Charguéraud, . Pottier, and . François, Functional translation of a calculus of capabilities, Pages 213?224 of: ACM International Conference on Functional Programming (ICFP), 2008.

D. G. Clarke, J. M. Potter, and J. Noble, Ownership types for flexible alias protection, Pages 48?64 of: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 1998.

K. Crary, . Walker, . David, and G. Morrisett, Typed memory management in a calculus of capabilities, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, 1999.
DOI : 10.1145/292540.292564

N. Danielsson, . Anders, and T. Altenkirch, Subtyping, declaratively. Pages 100?118 of: International Conference on Mathematics of Program Construction (MPC), Lecture Notes in Computer Science, vol.6120, 2010.

. De-bruijn and G. Nicolaas, Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem, Indag. Math, vol.34, issue.5, pp.381-392, 1972.

R. Deline and M. Fähndrich, Enforcing high-level protocols in low-level software, Pages 59?69 of: ACM Conference on Programming Language Design and Implementation (PLDI), 2001.

D. L. Detlefs, K. Leino, M. Rustan, and G. Nelson, Wrestling with rep exposure, 1998.

W. Dietl and M. Peter, Universes: Lightweight Ownership for JML., The Journal of Object Technology, vol.4, issue.8, pp.5-32, 2005.
DOI : 10.5381/jot.2005.4.8.a1

. Dinsdale-young, . Thomas, . Dodds, . Mike, . Gardner et al., Concurrent Abstract Predicates, 2010.
DOI : 10.1007/978-3-642-14107-2_24

. Dinsdale-young, . Thomas, . Birkedal, . Lars, . Gardner et al., Views: compositional reasoning for concurrent programs, 2012.

R. Dockins, . Hobor, . Aquinas, and A. W. Appel, A fresh look at separation algebras and share accounting. Pages 161?177 of: Asian Symposium on Programming Languages and Systems (APLAS), Lecture Notes in Computer Science, vol.5904, 2009.

M. Fähndrich and R. Deline, Adoption and focus: practical linear types for imperative programming, Pages 13?24 of: ACM Conference on Programming Language Design and Implementation (PLDI), 2002.

M. Fähndrich, . Aiken, . Mark, . Hawblitzel, . Chris et al., Language support for fast and reliable message-based communication in Singularity OS, 2006.

V. Gapeyev, . Levin, . Michael, . Pierce, and . Benjamin, Recursive subtyping revealed, Journal of Functional Programming, vol.12, issue.6, pp.511-548, 2002.

N. Gauthier, . Pottier, and . François, Numbering matters: First-order canonical forms for second-order recursive types, Pages 150?161 of: ACM International Conference on Functional Programming (ICFP), 2004.

D. K. Gifford, . Jouvelot, . Pierre, M. A. Sheldon, and J. W. Toole, Report on the FX-91 programming language, 1992.

J. Girard, Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, Thèse d'état, 1972.

N. Glew, A Theory of Second-Order Trees, Pages 147?161 of: European Symposium on Programming (ESOP). Lecture Notes in Computer Science, 2002.
DOI : 10.1007/3-540-45927-8_11

A. Gotsman, . Berdine, . Josh, . Cook, . Byron et al., Local Reasoning for Storable Locks and Threads, 2007.
DOI : 10.1007/978-3-540-76637-7_3

R. Harper, A simplified account of polymorphic references, Information Processing Letters, vol.51, issue.4, pp.201-206, 1994.
DOI : 10.1016/0020-0190(94)90120-1

C. A. Hoare, Proof of correctness of data representations, Acta Informatica, vol.4, pp.271-281, 1972.

A. Hobor, A. W. Appel, and F. Nardelli, Oracle Semantics for Concurrent Separation Logic, Pages 353?367 of: European Symposium on Programming (ESOP), 2008.
DOI : 10.1007/978-3-540-78739-6_27

M. Hofmann, A type system for bounded space and functional in-place update, Nordic Journal of Computing, vol.7, issue.4, pp.258-289, 2000.

J. Hogg, Islands: Aliasing protection in object-oriented languages, Pages 271?285 of: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 1991.

S. S. Ishtiaq, . Hearn, and W. Peter, BI as an assertion language for mutable data structures, Pages 14?26 of: ACM Symposium on Principles of Programming Languages (POPL), 2001.

J. Launchbury, S. Jones, and . Peyton, State in Haskell, LISP and Symbolic Computation, vol.2, issue.4, pp.293-341, 1995.
DOI : 10.1007/BF01018827

P. Levy and . Blain, Possible World Semantics for General Storage in Call-By-Value, Computer Science Logic. Lecture Notes in Computer Science, vol.2471, 2002.
DOI : 10.1007/3-540-45793-3_16

D. B. Macqueen, G. D. Plotkin, and R. Sethi, An ideal model for recursive polymorphic types, Information and Control, vol.71, issue.1-2, pp.95-130, 1986.
DOI : 10.1016/S0019-9958(86)80019-5

K. Mazurak, . Zhao, . Jianzhou, and S. Zdancewic, Lightweight linear types in system F ? . Pages 77?88 of: Workshop on Types in Language Design and Implementation (TLDI), 2010.

J. C. Mitchell, Polymorphic type inference and containment, Information and Computation, vol.76, issue.2-3, pp.2-3, 1988.
DOI : 10.1016/0890-5401(88)90009-0

S. Monnier, Statically tracking state with typed regions, 2008.

P. Müller and A. Poetzsch-heffter, Universes: A type system for alias and dependency control, 2001.

A. Nanevski, . Morrisett, . Greg, and L. Birkedal, Hoare type theory, polymorphism and separation, Journal of Functional Programming, vol.18, pp.5-6, 2008.

A. Nanevski, . Vafeiadis, . Viktor, and J. Berdine, Structuring the verification of heap-manipulating programs, Pages 261?274 of: ACM Symposium on Principles of Programming Languages (POPL), 2010.

O. Hearn and W. Peter, Resources, concurrency and local reasoning, Theoretical Computer Science, vol.375, pp.1-3, 2007.

O. Hearn, W. Peter, . Yang, . Hongseok, and J. C. Reynolds, Separation and information hiding, Pages 268?280 of: ACM Symposium on Principles of Programming Languages (POPL), 2004.

P. Jones, . Simon, and P. Wadler, Imperative functional programming, Pages 71?84 of: ACM Symposium on Principles of Programming Languages (POPL), 1993.

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

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

R. Pollack, . Sato, . Masahiko, and W. Ricciotti, A Canonical Locally Named Representation of Binding, Journal of Automated Reasoning, vol.40, issue.4, pp.185-207, 2012.
DOI : 10.1007/s10817-011-9229-y

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

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

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

F. Pottier, Accompanying Coq scripts; for browsing, 2012.

F. Pottier, Accompanying Coq scripts; for downloading Available at http: //gallium.inria.fr/~fpottier/ssphs/ssphs.tar.gz and also as an online supplement at http, 2012.

F. Pottier and J. Protzenko, Programming with permissions: an introduction to Mezzo, 2012.

B. Reus and . Schwinghammer, Separation logic for higher-order store. Pages 575?590 of: Computer Science Logic, Lecture Notes in Computer Science, vol.4207, 2006.

J. C. Reynolds, Towards a theory of type structure. Pages 408?425 of: Colloque sur la Programmation, Lecture Notes in Computer Science, vol.19, 1974.

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

J. Schwinghammer, . Birkedal, . Lars, . Reus, . Bernhard et al., Nested Hoare triples and frame rules for higher-order store. Pages 440?454 of: Computer Science Logic, Lecture Notes in Computer Science, vol.5771, 2009.

J. Schwinghammer, . Yang, . Hongseok, . Birkedal, . Lars et al., A Semantic Foundation for Hidden State, Pages 2?17 of: International Conference on Foundations of Software Science and Computation Structures (FOSSACS). Lecture Notes in Computer Science, 2010.
DOI : 10.1007/978-3-642-12032-9_2

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

J. Schwinghammer, . Birkedal, . Lars, . Pottier, . François et al., A step-indexed Kripke model of hidden state, Mathematical Structures in Computer Science, 2012.
DOI : 10.1145/504709.504712

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

. Smith, . Frederick, . Walker, . David, and G. Morrisett, Alias Types, Pages 366?381 of: European Symposium on Programming (ESOP), 2000.
DOI : 10.1007/3-540-46425-5_24

. Swamy, . Nikhil, . Hicks, . Michael, . Morrisett et al., Safe manual memory management in Cyclone, Science of Computer Programming, vol.62, issue.2, pp.122-144, 2006.
DOI : 10.1016/j.scico.2006.02.003

J. Talpin and P. Jouvelot, The type and effect discipline, Information and Computation, vol.11, issue.2, pp.245-296, 1994.

. Tan, . Gang, . Shao, . Zhong, . Feng et al., Weak updates and separation logic. Pages 178?193 of: Asian Symposium on Programming Languages and Systems (APLAS), Lecture Notes in Computer Science, vol.5904, 2009.

M. Tofte, . Talpin, and . Jean-pierre, Region-Based Memory Management, Information and Computation, vol.132, issue.2, pp.109-176, 1997.
DOI : 10.1006/inco.1996.2613

J. A. Tov and R. Pucella, Stateful Contracts for Affine Types, Pages 550?569 of: European Symposium on Programming (ESOP), 2010.
DOI : 10.1007/978-3-642-11957-6_29

C. Urban, Nominal Techniques in Isabelle/HOL, Journal of Automated Reasoning, vol.323, issue.1???2, pp.327-356, 2008.
DOI : 10.1007/s10817-008-9097-2

J. Vouillon, . Melliès, and . Paul-andré, Semantic types: a fresh look at the ideal model for types, Pages 52?63 of: ACM Symposium on Principles of Programming Languages (POPL), 2004.
URL : https://hal.archives-ouvertes.fr/hal-00150968

D. Walker, Substructural type systems Advanced Topics in Types and Programming Languages, pp.3-43, 2005.

D. Walker and G. Morrisett, Alias types for recursive data structures. Pages 177?206 of: Workshop on Types in Compilation (TIC), Lecture Notes in Computer Science, vol.2071, 2000.

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

A. K. Wright and M. Felleisen, A Syntactic Approach to Type Soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994.
DOI : 10.1006/inco.1994.1093