An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576580-583, 1969. ,
Some techniques for proving correctness of programs which alter data structures, Machine Intelligence, vol.7, p.2350, 1972. ,
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
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
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
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
The essence of compiling with continuations, SIGPLAN Not, vol.28, issue.6, p.237247, 1993. ,
Types and Programming Languages, 2002. ,
Unify and conquer, Proceedings of the 1990 ACM conference on LISP and functional programming , LFP '90, p.218226, 1990. ,
DOI : 10.1145/91556.91652
Polymorphic eect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages . POPL '88, p.4757, 1988. ,
Region-Based Memory Management, Information and Computation, vol.132, issue.2, 1997. ,
DOI : 10.1006/inco.1996.2613
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
Typed regions In: Second workshop on Semantics, Program Analysis, and Computing Environments for Memory Management, 2004. ,
Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems, vol.24, issue.3, p.217298, 2002. ,
Region-based shape analysis with tracked locations, SIG- PLAN Not, vol.40, issue.1, p.310323, 2005. ,
Eective typestate verication in the presence of aliasing, ACM Trans. Softw. Eng. Methodol, vol.1719, issue.9, p.34, 2008. ,
Alias Analysis for Object-Oriented Programs, 196232. ,
DOI : 10.1007/978-3-642-36946-9_8
Ownership Types: A Survey, pp.31-1558 ,
DOI : 10.1007/978-3-642-36946-9_3
Notions of Aliasing and Ownership, pp.31-5983 ,
DOI : 10.1007/978-3-642-36946-9_4
Object ownership in program verication, pp.31-289318 ,
Islands: Aliasing protection in object-oriented languages, SIGPLAN Not, vol.26, issue.11, p.271285, 1991. ,
Balloon types: Controlling sharing of state in data types, Proceedings ECOOP'97, p.3259, 1997. ,
DOI : 10.1007/BFb0053373
Ownership transfer in universe types, ACM SIGPLAN conference on Object-oriented programming systems and applications (OOPSLA), p.461478, 2007. ,
Linear types can change the world! In: Programming Concepts and Methods, p.North, 1990. ,
???Use-once??? variables and linear objects, ACM SIGPLAN Notices, vol.30, issue.1, p.4552, 1995. ,
DOI : 10.1145/199818.199860
Alias burying: Unique variables without destructive reads, Software: Practice and Experience, vol.34, issue.6, p.533553, 2001. ,
DOI : 10.1002/spe.370
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
Functional translation of a calculus of capabilities, ACM SIGPLAN International Conference on Functional Programming (ICFP) ,
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
The spirit of ghost code, 26th International Conference on Computer Aided Verication ,
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