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

T. Balabonski, F. Pottier, and J. Protzenko, The Design and Formalization of Mezzo, a Permission-Based Programming Language, ACM Transactions on Programming Languages and Systems, vol.38, issue.4, 2014.
DOI : 10.1145/2837022
URL : https://hal.archives-ouvertes.fr/hal-01246534

C. Berdine, P. W. Calcagno, and . Hearn, Smallfoot: Modular Automatic Assertion Checking with Separation Logic, Formal Methods for Components and Objects, pp.115-137, 2005.
DOI : 10.1007/11804192_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.63.613

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

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

B. Delaware, C. D. Bruno, T. Oliveira, and . Schrijvers, Meta-theory à la carte, Principles of Programming Languages (POPL), pp.207-218, 2013.
DOI : 10.1145/2429069.2429094

A. Guéneau, F. Pottier, and J. Protzenko, The ins and outs of iteration in Mezzo. Higher-Order Programming and Effects (HOPE), p.4, 2013.

B. Jones, Specification and design of (parallel) programs, IFIP congress, pp.321-332, 1983.

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

J. Protzenko, Mezzo: a typed language for safe effectful concurrent programs, 2014.
URL : https://hal.archives-ouvertes.fr/tel-01086106

J. Protzenko, Mezzo-web: try Mezzo in your browser, 2014.

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), pp.366-381, 2000.
DOI : 10.1007/3-540-46425-5_24

M. Swamy, G. Hicks, D. Morrisett, T. Grossman, and . 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