P. Achten and M. J. Plasmeijer, Abstract, Journal of Functional Programming, vol.27, issue.01, pp.81-110, 1995.
DOI : 10.1109/LICS.1989.39155

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

A. Amighi and C. Haack, Marieke Huisman, and Clément Hurlin. 2015. Permission-based separation logic for multithreaded Java programs, Logical Methods in Computer Science, vol.11, issue.1, pp.1-66, 2015.

T. Antonopoulos, N. Gorogiannis, C. Haase, M. I. Kanovich, and J. Ouaknine, Foundations for Decision Problems in Separation Logic with General Inductive Predicates, Foundations of Software Science and Computation Structures (FOSSACS), pp.411-425, 2014.
DOI : 10.1007/978-3-642-54830-7_27

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

T. Balabonski, F. Pottier, and J. Protzenko, Type Soundness and Race Freedom for Mezzo, Proceedings of the 12th International Symposium on Functional and Logic Programming (FLOPS 2014), pp.253-269, 2014.
DOI : 10.1007/978-3-319-07151-0_16

URL : https://hal.archives-ouvertes.fr/hal-01081194

A. Barber, Dual Intuitionistic Linear Logic, 1996.

J. Berdine, C. Calcagno, and P. W. Hearn, A Decidable Fragment of Separation Logic, Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pp.97-109, 2004.
DOI : 10.1007/978-3-540-30538-5_9

J. Berdine, C. Calcagno, and P. W. Hearn, Smallfoot: Modular Automatic Assertion Checking with Separation Logic, Formal Methods for Components and Objects, pp.115-137, 2005.
DOI : 10.1007/11804192_6

J. Berdine, C. Calcagno, and P. W. Hearn, Symbolic Execution with Separation Logic, Asian Symposium on Programming Languages and Systems (APLAS), pp.52-68, 2005.
DOI : 10.1007/11575467_5

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

K. Bierhoff, N. E. Beckman, and J. Aldrich, Practical API Protocol Checking with Access Permissions, European Conference on Object-Oriented Programming (ECOOP), pp.195-219, 2009.
DOI : 10.1109/TSE.1986.6312929

K. Bierhoff, N. E. Beckman, and J. Aldrich, Checking Concurrent Typestate with Access Permissions in Plural: A Retrospective, Engineering of Software, pp.35-48, 2011.
DOI : 10.1007/978-3-642-19823-6_4

L. Birkedal, B. R. Schwinghammer, K. Støvring, J. Thamsborg, and H. Yang, Step-indexed Kripke models over recursive worlds, Principles of Programming Languages (POPL), pp.119-132, 2011.

L. Robert and . Bocchino-jr, Alias Control for Deterministic Parallelism, Aliasing in Object-Oriented Programming. Types, 2013.

L. Robert, . Bocchino-jr, S. Vikram, and . Adve, Types, Regions, and Effects for Safe Programming with Object-Oriented Parallel Frameworks, European Conference on Object-Oriented Programming (ECOOP), pp.306-332, 2011.

L. Robert, . Bocchino-jr, S. Vikram, S. V. Adve, M. Adve et al., Parallel Programming Must Be Deterministic by Default, USENIX Conference on Hot Topics in Parallelism (HotPar, pp.1-6, 2009.

L. Robert, . Bocchino-jr, S. Vikram, D. Adve, S. V. Dig et al., A type and effect system for deterministic parallel Java, Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp.97-116, 2009.

L. Robert, . Bocchino-jr, N. Stephen-heumann, S. V. Honarmand, V. S. Adve et al., Safe nondeterminism in a deterministic-by-default parallel language, Principles of Programming Languages (POPL, pp.535-548, 2011.

R. Bornat, C. Calcagno, O. Peter, M. Hearn, and . Parkinson, Permission accounting in separation logic, Principles of Programming Languages (POPL), pp.259-270, 2005.

C. Boyapati, R. Lee, and M. Rinard, Ownership types for safe programming: preventing data races and deadlocks, Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp.211-230, 2002.

J. Boyland, Checking Interference with Fractional Permissions, Static Analysis Symposium (SAS), pp.55-72, 2003.
DOI : 10.1007/3-540-44898-5_4

J. Tang and B. , Semantics of fractional permissions with nesting, ACM Transactions on Programming Languages and Systems, vol.32, issue.22, pp.1-2233, 2010.

T. Braibant and D. Pous, Tactics for Reasoning Modulo AC in Coq, Certified Programs and Proofs, pp.167-182, 2011.
DOI : 10.1007/978-3-540-71067-7_23

URL : https://hal.archives-ouvertes.fr/hal-00484871

D. Stephen and . Brookes, A Semantics for Concurrent Separation Logic, International Conference on Concurrency Theory (CONCUR), pp.16-34, 2004.

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

C. Calcagno, D. Distefano, O. Peter, and . Hearn, Open-sourcing Facebook In- fer: Identify bugs before you ship. https://code.facebook.com/posts/1648953042007882/ open-sourcing-facebook-infer-identify-bugs-before-you-ship, 2015.

. Bor-yuh-evan, X. Chang, and . Rival, Relational inductive shape analysis, Principles of Programming Languages (POPL), pp.247-260, 2008.

A. Charguéraud, Characteristic Formulae for Mechanized Program Verification, 2010.

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.

J. Chrzaszcz, Polymorphic subtyping without distributivity, International Symposium on Mathematical Foundations of Computer Science, pp.346-355, 1998.
DOI : 10.1007/BFb0055784

D. Clarke, S. Drossopoulou, and J. Noble, Aliasing, Confinement, and Ownership in Object-Oriented Programming, Object-Oriented Technology. ECOOP 2003 Workshop Reader, pp.197-207, 2004.
DOI : 10.1007/978-3-540-25934-3_19

D. Clarke, J. Östlund, I. Sergey, and T. Wrigstad, Ownership Types: A Survey, Aliasing in Object-Oriented Programming, pp.15-58, 2013.
DOI : 10.1007/978-3-642-36946-9_3

D. Clarke and T. Wrigstad, External Uniqueness Is Unique Enough, European Conference on Object-Oriented Programming (ECOOP), pp.176-200, 2003.
DOI : 10.1007/978-3-540-45070-2_9

D. G. Clarke, J. Noble, and J. Potter, Simple Ownership Types for Object Containment, European Conference on Object-Oriented Programming (ECOOP), pp.53-76, 2001.
DOI : 10.1007/3-540-45337-7_4

D. G. Clarke, J. M. Potter, and J. Noble, Ownership types for flexible alias protection, Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp.48-64, 1998.

E. Cohen, M. Dahlweid, M. A. Hillebrand, D. Leinenbach, M. Moskal et al., VCC: A Practical System for Verifying Concurrent C, Theorem Proving in Higher Order Logics (TPHOLs), pp.23-42, 2009.
DOI : 10.1007/978-3-540-74591-4_15

B. Cook, C. Haase, J. Ouaknine, M. J. Parkinson, and J. Worrell, Tractable Reasoning in a Fragment of Separation Logic, International Conference on Concurrency Theory (CON- CUR), pp.235-249, 2011.
DOI : 10.1007/3-540-45294-X_10

L. Damas, Type Assignment in Programming Languages, 1985.

B. Delaware, C. D. Bruno, T. Oliveira, and . Schrijvers, Meta-theory à La Carte, Principles of Programming Languages (POPL), pp.207-218, 2013.

R. Deline and M. Fähndrich, Enforcing High-Level Protocols in Low-Level Software, Programming Language Design and Implementation (PLDI), pp.59-69, 2001.

L. David, K. Detlefs, M. Rustan, G. Leino, and . Nelson, Wrestling with rep exposure, 1998.

W. Dietl and P. Müller, Universes: Lightweight Ownership for JML., The Journal of Object Technology, vol.4, issue.8, pp.5-32, 2005.
DOI : 10.5381/jot.2005.4.8.a1

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.

T. Dinsdale-young, M. Dodds, P. Gardner, M. J. Parkinson, and V. Vafeiadis, Concurrent Abstract Predicates, European Conference on Object-Oriented Programming (ECOOP), pp.504-528, 2010.
DOI : 10.1007/978-3-642-14107-2_24

D. Distefano and M. J. Parkinson, jStar: towards practical verification for Java, Object- Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp.213-226, 2008.

R. Dockins, A. Hobor, and A. W. Appel, A Fresh Look at Separation Algebras and Share Accounting, Asian Symposium on Programming Languages and Systems (APLAS), pp.161-177, 2009.
DOI : 10.1007/978-3-642-10672-9_13

J. Filliâtre, L. Gondelman, and A. Paskevich, The Spirit of Ghost Code, Computer Aided Verification, pp.1-16, 2014.
DOI : 10.1007/978-3-319-08867-9_1

C. Flanagan and M. Abadi, Types for Safe Locking, European Symposium on Programming (ESOP), pp.91-108, 1999.
DOI : 10.1007/3-540-49099-X_7

M. Fähndrich, M. Aiken, C. Hawblitzel, O. Hodson, G. Hunt et al., Language support for fast and reliable message-based communication in Singularity OS, EuroSys, pp.177-190, 2006.

M. Fähndrich and R. Deline, Adoption and focus: practical linear types for imperative programming, Programming Language Design and Implementation (PLDI), pp.13-24, 2002.

C. S. Gordon, M. J. Parkinson, J. Parsons, A. Bromfield, and J. Duffy, Uniqueness and reference immutability for safe parallelism, Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp.21-40, 2012.

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

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.

C. Haack, M. Huisman, and C. Hurlin, Reasoning about Java???s Reentrant Locks, Asian Symposium on Programming Languages and Systems (APLAS), pp.171-187, 2008.
DOI : 10.1016/j.tcs.2006.12.035

C. Haack and C. Hurlin, Resource Usage Protocols for Iterators., The Journal of Object Technology, vol.8, issue.4, pp.55-83, 2009.
DOI : 10.5381/jot.2009.8.4.a3

URL : https://hal.archives-ouvertes.fr/inria-00410128

S. Heule, K. Rustan, M. Leino, P. Müller, and A. J. Summers, Abstract Read Permissions: Fractional Permissions without the Fractions, Verification, Model Checking and Abstract Interpretation (VMCAI), pp.315-334, 2013.
DOI : 10.1007/978-3-642-35873-9_20

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

B. Jacobs, D. Bosnacki, and R. Kuipe, Modular Termination Verification, European Conference on Object-Oriented Programming (ECOOP) (Leibniz International Proceedings in Informatics), pp.99-1023, 2015.

B. Jacobs and F. Piessens, The VeriFast Program Verifier, 2008.

R. Neelakantan, J. Krishnaswami, L. Aldrich, K. Birkedal, A. Svendsen et al., Design Patterns in Separation Logic, Types in Language Design and Implementation (TLDI), pp.105-116, 2009.

M. Rustan, P. Leino, and . Müller, A Basis for Verifying Multi-threaded Programs, European Symposium on Programming (ESOP), pp.378-393, 2009.

M. Rustan, P. Leino, J. Müller, and . Smans, Deadlock-Free Channels and Locks, European Symposium on Programming (ESOP), pp.407-426, 2010.

T. Maeda, H. Sato, and A. Yonezawa, Extended alias type system using separating implication, Proceedings of the 7th ACM SIGPLAN workshop on Types in language design and implementation, TLDI '11, pp.29-42, 2011.
DOI : 10.1145/1929553.1929559

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

R. Milner, A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, issue.3, pp.348-375, 1978.
DOI : 10.1016/0022-0000(78)90014-4

Y. Minamide, A functional representation of data structures with a hole, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.75-84, 1998.
DOI : 10.1145/268946.268953

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

P. Müller and A. Rudich, Ownership transfer in universe types, Object-Oriented Programming , Systems, Languages, and Applications (OOPSLA), pp.461-478, 2007.

K. Naden, R. Bocchino, J. Aldrich, and K. Bierhoff, A type system for borrowing permissions, Principles of Programming Languages (POPL), pp.557-570, 2012.

A. Nanevski, V. Vafeiadis, and J. Berdine, Structuring the verification of heapmanipulating programs, Principles of Programming Languages (POPL), pp.261-274, 2010.

J. A. , N. Pérez, and A. Rybalchenko, Separation logic + superposition calculus = heap theorem prover, Programming Language Design and Implementation (PLDI), pp.556-566, 2011.

W. O. Peter and . Hearn, Resources, Concurrency and Local Reasoning, Theoretical Computer Science, vol.375, pp.1-3, 2007.

S. Peyton, J. , and P. Wadler, Imperative functional programming, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '93, pp.71-84, 1993.
DOI : 10.1145/158511.158524

R. Piskac, T. Wies, and D. Zufferey, Automating Separation Logic Using SMT, Computer Aided Verification, pp.773-789, 2013.
DOI : 10.1007/978-3-642-39799-8_54

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

F. Pottier and J. Protzenko, A few lessons from the Mezzo project, Summit on Advances in Programming Languages (SNAPL), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01246360

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

J. Protzenko, A Mezzo sample project, 2014.

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.

J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang, Nested Hoare Triples and Frame Rules for Higher-Order Store, In Computer Science Logic (Lecture Notes in Computer Science), vol.11, issue.4, pp.440-454, 2009.
DOI : 10.1142/6284

J. Schwinghammer, H. Yang, L. Birkedal, F. Pottier, and B. Reus, A Semantic Foundation for Hidden State, Foundations of Software Science and Computation Structures (FOSSACS), pp.2-17, 2010.
DOI : 10.1007/978-3-642-12032-9_2

S. Smetsers, E. Barendsen, C. J. Marko, M. J. Van-eekelen, and . Plasmeijer, Guaranteeing safe destructive updates through a type system with uniqueness information for graphs, In Dagstuhl Seminar on Graph Transformations in Computer Science (Lecture Notes in Computer Science), vol.776, pp.358-379, 1994.
DOI : 10.1007/3-540-57787-4_23

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

K. Svendsen and L. Birkedal, Impredicative Concurrent Abstract Predicates, European Symposium on Programming (ESOP), pp.149-168, 2014.
DOI : 10.1007/978-3-642-54833-8_9

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

M. Tofte, Operational Semantics and Polymorphic Type Inference, Ph.D. Dissertation, 1988.

M. Tofte and J. Talpin, Implementation of the typed call-by-value ??-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '94, pp.188-201, 1994.
DOI : 10.1145/174675.177855

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

J. A. Tov and R. Pucella, Practical Affine Types, Principles of Programming Languages (POPL), pp.447-458, 2011.

S. Matthew, M. D. Tschantz, and . Ernst, Javari: adding reference immutability to Java, Object- Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp.211-230, 2005.

T. Tuerk, Local reasoning about while-loops Unpublished, 2010.

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.

V. Vafeiadis, Concurrent Separation Logic and Operational Semantics, Electronic Notes in Theoretical Computer Science, vol.276, pp.335-351, 2011.
DOI : 10.1016/j.entcs.2011.09.029

J. Vitek and B. Bokowski, Confined types in Java, Software: Practice and Experience, vol.33, issue.6, pp.507-532, 2001.
DOI : 10.1002/spe.369

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

D. Walker, K. Crary, and G. Morrisett, Typed memory management via static capabilities, ACM Transactions on Programming Languages and Systems, vol.22, issue.4, pp.701-771, 2000.
DOI : 10.1145/363911.363923

D. Walker and G. Morrisett, Alias Types for Recursive Data Structures, Types in Compilation (TIC), pp.177-206, 2000.
DOI : 10.1007/3-540-45332-6_7

K. Andrew and . Wright, Simple Imperative Polymorphism, Lisp and Symbolic Computation, pp.343-356, 1995.

K. Andrew, M. Wright, and . Felleisen, A Syntactic Approach to Type Soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994.

A. Proof, . Of, and . Soundness, We outline the main steps along the way that leads to the statement of type soundness (Theorem A.13)