A. Ahmed, D. Dreyer, and A. Rossberg, State-dependent representation independence, ACM Symposium on Principles of Programming Languages (POPL), pp.340-353, 2009.
DOI : 10.1145/1480881.1480925
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.144.2285

R. Atkey, Amortised Resource Analysis with Separation Logic, European Symposium on Programming, pp.85-103, 2010.
DOI : 10.1007/978-3-642-11957-6_6
URL : http://arxiv.org/abs/1104.1998

A. Charguéraud and F. Pottier, Functional translation of a calculus of capabilities, ACM International Conference on Functional Programming (ICFP), pp.213-224, 2008.

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

K. Crary and S. Weirich, Resource bound certification, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, pp.184-198, 2000.
DOI : 10.1145/325694.325716

N. Anders-danielsson, Lightweight semiformal time complexity analysis for purely functional data structures, ACM Symposium on Principles of Programming Languages (POPL), 2008.

M. Dodds, X. Feng, M. J. Parkinson, and V. Vafeiadis, Deny-Guarantee Reasoning, European Symposium on Programming (ESOP), pp.363-377, 2009.
DOI : 10.1007/978-3-642-00590-9_26
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.148.980

V. Dornic, P. Jouvelot, and D. K. Gifford, Polymorphic time systems for estimating program complexity, ACM Letters on Programming Languages and Systems, vol.1, issue.1, pp.33-45, 1992.
DOI : 10.1145/130616.130620

D. Dreyer, G. Neis, and L. Birkedal, The impact of higherorder state and control effects on local relational reasoning, ACM International Conference on Functional Programming (ICFP), pp.143-156, 2010.

M. Fähndrich and R. Leino, Heap monotonic typestates, International Workshop on Alias Confinement and Ownership (IWACO), 2003.

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=10.1.1.100.6546

C. R. Eric and . Hehner, Abstractions of Time, pp.191-210, 1994.

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

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.

T. Gary, A. L. Leavens, and . Baker, Enhancing the pre-and postcondition technique for more expressive specifications, Formal Methods (FM), pp.1087-1106, 1999.

K. Rustan, M. Leino, and W. Schulte, Using history invariants to verify observers, European Symposium on Programming (ESOP), pp.80-94, 2007.

B. Liskov and J. M. Wing, A behavioral notion of subtyping, ACM Transactions on Programming Languages and Systems, vol.16, issue.6, pp.1811-1841, 1994.
DOI : 10.1145/197320.197383

K. Mazurak, J. Zhao, and S. Zdancewic, Lightweight linear types in system F ?, Workshop on Types in Language Design and Implementation (TLDI), pp.77-88, 2010.

A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal, Abstract Predicates and Mutable ADTs in Hoare Type Theory, European Symposium on Programming (ESOP), pp.189-204, 2007.
DOI : 10.1007/978-3-540-71316-6_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.142.2782

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

C. Okasaki, Purely Functional Data Structures, 1999.
DOI : 10.1017/CBO9780511530104
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.505

C. Benjamin, D. N. Pierce, and . Turner, Simple type-theoretic foundations for object-oriented programming, Journal of Functional Programming, vol.4, issue.2, pp.207-247, 1994.

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, 2009.

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

B. Reistad and D. K. Gifford, Static dependent costs for estimating execution time, ACM Symposium on Lisp and Functional Programming (LFP), pp.65-78, 1994.

F. B. Schneider, On concurrent programming, Communications of the ACM, vol.41, issue.4, 1997.
DOI : 10.1145/273035.273072

F. Smith, D. Walker, and G. Morrisett, Alias Types, European Symposium on Programming, pp.366-381, 2000.
DOI : 10.1007/3-540-46425-5_24

E. Sumii, A Complete Characterization of Observational Equivalence in Polymorphic ??-Calculus with General References, Computer Science Logic, pp.455-469, 2009.
DOI : 10.1016/j.tcs.2006.12.032

. Robert-endre-tarjan, Amortized Computational Complexity, SIAM Journal on Algebraic Discrete Methods, vol.6, issue.2, pp.306-318, 1985.
DOI : 10.1137/0606031

H. Xi, Dependent ML An approach to practical programming with dependent types, Journal of Functional Programming, vol.17, issue.02, pp.215-286, 2007.
DOI : 10.1017/S0956796806006216