C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576580-583, 1969.

R. Burstall, Some techniques for proving correctness of programs which alter data structures, Machine Intelligence, vol.7, p.2350, 1972.

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

I. T. Kassios, Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions, 14th International Symposium on Formal Methods (FM'06, p.268283, 2006.
DOI : 10.1007/11813040_19

J. C. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, p.125128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

J. Berdine and P. W. O-'hearn, Strong Update, Disposal, and Encapsulation in Bunched Typing, Electronic Notes in Theoretical Computer Science, vol.158, p.8198, 2006.
DOI : 10.1016/j.entcs.2006.04.006

C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen, The essence of compiling with continuations, SIGPLAN Not, vol.28, issue.6, p.237247, 1993.

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

H. G. Baker, Unify and conquer, Proceedings of the 1990 ACM conference on LISP and functional programming , LFP '90, p.218226, 1990.
DOI : 10.1145/91556.91652

J. M. Lucassen and D. K. Giord, Polymorphic eect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages . POPL '88, p.4757, 1988.

M. Tofte and J. P. Talpin, Region-Based Memory Management, Information and Computation, vol.132, issue.2, 1997.
DOI : 10.1006/inco.1996.2613

F. Smith, D. Walker, and J. G. Morrisett, Alias Types, Programming Languages and Systems, 9th European Symposium on Programming, ESOP 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, 2000.
DOI : 10.1007/3-540-46425-5_24

S. Monnier, Typed regions In: Second workshop on Semantics, Program Analysis, and Computing Environments for Memory Management, 2004.

M. Sagiv, T. W. Reps, and R. Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems, vol.24, issue.3, p.217298, 2002.

B. Hackett and R. Rugina, Region-based shape analysis with tracked locations, SIG- PLAN Not, vol.40, issue.1, p.310323, 2005.

S. J. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay, Eective typestate verication in the presence of aliasing, ACM Trans. Softw. Eng. Methodol, vol.1719, issue.9, p.34, 2008.

M. Sridharan, S. Chandra, J. Dolby, S. J. Fink, and E. Yahav, Alias Analysis for Object-Oriented Programs, 196232.
DOI : 10.1007/978-3-642-36946-9_8

D. Clarke, J. Östlund, I. Sergey, and T. Wrigstad, Ownership Types: A Survey, pp.31-1558
DOI : 10.1007/978-3-642-36946-9_3

A. Mycroft and J. Voigt, Notions of Aliasing and Ownership, pp.31-5983
DOI : 10.1007/978-3-642-36946-9_4

W. Dietl and P. Müller, Object ownership in program verication, pp.31-289318

J. Hogg, Islands: Aliasing protection in object-oriented languages, SIGPLAN Not, vol.26, issue.11, p.271285, 1991.

P. S. Almeida, Balloon types: Controlling sharing of state in data types, Proceedings ECOOP'97, p.3259, 1997.
DOI : 10.1007/BFb0053373

P. Müller and A. Rudich, Ownership transfer in universe types, ACM SIGPLAN conference on Object-oriented programming systems and applications (OOPSLA), p.461478, 2007.

P. Wadler, Linear types can change the world! In: Programming Concepts and Methods, p.North, 1990.

H. G. Baker, ???Use-once??? variables and linear objects, ACM SIGPLAN Notices, vol.30, issue.1, p.4552, 1995.
DOI : 10.1145/199818.199860

J. Boyland, Alias burying: Unique variables without destructive reads, Software: Practice and Experience, vol.34, issue.6, p.533553, 2001.
DOI : 10.1002/spe.370

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, p.262275, 1999.
DOI : 10.1145/292540.292564

A. Charguéraud and F. Pottier, Functional translation of a calculus of capabilities, ACM SIGPLAN International Conference on Functional Programming (ICFP)

F. Bobot, J. C. Filliâtre, C. Marché, and A. Paskevich, Why3: Shepherd your herd of provers, Boogie 2011: First International Workshop on Intermediate Verication Languages, p.5364, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

J. C. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code, 26th International Conference on Computer Aided Verication

D. Clarke, J. Noble, and T. Wrigstad, Aliasing in Object-Oriented Programming: Types, Analysis and Verication, Lecture Notes in Computer Science, vol.7850, 2013.
DOI : 10.1007/978-3-642-36946-9