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

J. Aldrich, J. Sunshine, D. Saini, and Z. Sparks, Typestate-oriented programming, Proceeding of the 24th ACM SIGPLAN conference companion on Object oriented programming systems languages and applications, OOPSLA '09, pp.1015-1022, 2009.
DOI : 10.1145/1639950.1640073

M. Barnett, K. Rustan, M. Leino, and W. Schulte, The Spec# Programming System: An Overview, Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS), pp.49-69, 2004.
DOI : 10.1007/978-3-540-30569-9_3

J. Berdine, C. Calcagno, and P. W. Hearn, Smallfoot: Modular Automatic Assertion Checking with Separation Logic, Formal Methods for Components and Objects, pp.115-137, 2005.
DOI : 10.1007/11804192_6

K. Bierhoff and J. Aldrich, Modular typestate checking of aliased objects, Object-Oriented Programming, Systems, Languages , and Applications (OOPSLA), pp.301-320, 2007.

K. Bierhoff, N. E. Beckman, and J. Aldrich, Practical API Protocol Checking with Access Permissions, European Conference on Object-Oriented Programming, pp.195-219, 2009.
DOI : 10.1109/TSE.1986.6312929

J. Tang and B. , Semantics of fractional permissions with nesting, ACM Transactions on Programming Languages and Systems, vol.32, issue.6, 2010.

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

A. Charguéraud, Characteristic Formulae for Mechanized Program Verification, 2010.

D. G. Clarke, J. M. Potter, and J. Noble, Ownership types for flexible alias protection, Object-Oriented Programming, Systems , Languages, and Applications (OOPSLA), pp.48-64, 1998.

K. Crary, D. Walker, 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, pp.262-275, 1999.
DOI : 10.1145/292540.292564

R. Deline and M. Fähndrich, Enforcing high-level protocols in low-level software, Programming Language Design and Implementation (PLDI), pp.59-69, 2001.

R. Deline and M. Fähndrich, Typestates for Objects, European Conference on Object-Oriented Programming, pp.465-490, 2004.
DOI : 10.1007/978-3-540-24851-4_21

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

M. Fähndrich, M. Aiken, C. Hawblitzel, O. Hodson, G. Hunt et al., Language support for fast and reliable message-based communication in Singularity OS, EuroSys, pp.177-190, 2006.

M. Fähndrich and R. Deline, Adoption and focus: practical linear types for imperative programming, Programming Language Design and Implementation (PLDI), pp.13-24, 2002.

C. S. Gordon, M. J. Parkinson, J. Parsons, A. Bromfield, and J. Duffy, Uniqueness and reference immutability for safe parallelism, Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp.21-40, 2012.

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

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

B. Jacobs and F. Piessens, The VeriFast program verifier, 2008.

T. Maeda, H. Sato, and A. Yonezawa, Extended alias type system using separating implication, Proceedings of the 7th ACM SIGPLAN workshop on Types in language design and implementation, TLDI '11, 2011.
DOI : 10.1145/1929553.1929559

Y. Minamide, A functional representation of data structures with a hole, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.75-84, 1998.
DOI : 10.1145/268946.268953

P. Müller and A. Rudich, Ownership transfer in universe types, Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp.461-478, 2007.

K. Naden, R. Bocchino, J. Aldrich, and K. Bierhoff, A type system for borrowing permissions, Principles of Programming Languages (POPL), pp.557-570, 2012.

W. O. Peter and . Hearn, Resources, concurrency and local reasoning, Theoretical Computer Science, vol.375, issue.13, pp.271-307, 2007.

F. Pottier, Type soundness for Core Mezzo. Unpublished, 2013.

F. Pottier and J. Protzenko, Programming with permissions in Mezzo (long version) Unpublished, 2013.

C. John and . Reynolds, Separation logic: A logic for shared mutable data structures, Logic in Computer Science (LICS), pp.55-74, 2002.

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

N. Swamy, J. Chen, C. Fournet, P. Strub, K. Bhargavan et al., Secure distributed programming with value-dependent types, International Conference on Functional Programming (ICFP), pp.266-278, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00939188

N. Swamy, M. Hicks, G. Morrisett, D. Grossman, and T. Jim, 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. A. Tov and R. Pucella, Practical affine types, Principles of Programming Languages (POPL), pp.447-458, 2011.

T. Tuerk, Local reasoning about while-loops. Unpublished, 2010.

D. Walker and G. Morrisett, Alias Types for Recursive Data Structures, Types in Compilation (TIC), volume 2071 of Lecture Notes in Computer Science, pp.177-206, 2000.
DOI : 10.1007/3-540-45332-6_7