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

T. Balabonski and F. Pottier, A Coq formalization of Mezzo, 2013.

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 and F. Pottier, Functional translation of a calculus of capabilities, International Conference on Functional Programming (ICFP), pp.213-224, 2008.

A. Chlipala, Certified Programming and Dependent Types, 2013.

B. S. Delaware, B. C. Oliveira, and T. Schrijvers, Meta-theory à la carte, Principles of Programming Languages (POPL), pp.207-218, 2013.

T. Dinsdale-young, L. Birkedal, P. Gardner, M. J. Parkinson, and H. Yang, Views: compositional reasoning for concurrent programs, Principles of Programming Languages (POPL), pp.287-300, 2013.

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

P. D. Mosses, Modular structural operational semantics, Journal of Logic and Algebraic Programming, vol.6061, pp.195-228, 2004.

O. 'hearn and P. W. , Resources, concurrency and local reasoning, Theoretical Computer Science, vol.37513, pp.271-307, 2007.

F. Pottier, Syntactic soundness proof of a type-and-capability system with hidden state, Journal of Functional Programming, vol.4, issue.01, pp.38-144, 2013.
DOI : 10.1016/j.scico.2006.02.003
URL : https://hal.archives-ouvertes.fr/hal-00877589

F. Pottier and J. Protzenko, Programming with permissions in Mezzo, International Conference on Functional Programming (ICFP), pp.173-184, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00877590

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

A. Turon, D. Dreyer, and L. Birkedal, Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency, International Conference on Functional Programming (ICFP), pp.377-390, 2013.