.. Non-determinism-in-the-type-checker, 150 10.8 Propagating the expected type, p.151

.. Using-a-write-once-reference, 25 3.2 Implementation of write-once references, p.26

.. Ill-typed-code, 29 3.6 Fixing the racy program, using a lock, 30 3.7 Hiding internal state via a lock, p.30

.. Axiomatization-of-nesting-in-mezzo, 49 4.2 A union-find data structure implemented with nesting (interface) 51 4.3 A union-find data structure implemented with nesting, p.52

.. The-type-of-rich-booleans, 57 4.7 A program involving conjunction rejected by the type-checker, p.58

C. Axiomatization-of, 60 4.10 Specialized implementation of a channel (interface) Implementation of a server using mychannel, p.62

.. Landin-'s-knot, 166 11.7 A complete subtraction example (kinds omitted for readability) 168 11.8 A valid Mezzo program that can't be type-checked 172 11.9 The interface of the Derivations module 173 12.1 First merge example 176 12.2 Second merge example, 176 12.5 Computing the ? function

[. Bibliography, . Aiken, S. Jeffrey, J. Foster, T. Kodumal et al., Checking and inferring local non-aliasing, ACM SIGPLAN Notices, vol.38, issue.5, pp.129-140, 2003.

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

J. Aldrich, Resource-based programming in Plaid. Fun Ideas and Thoughts, 2010.

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

G. Henry and . Baker, Unify and conquer (garbage, updating, aliasing, ...) in functional languages, ACM Symposium on Lisp and Functional Programming (LFP), pp.218-226, 1990.

[. 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

[. 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

J. Brotherston, C. Fuhs, N. Gorogiannis, and J. Perez, A decision procedure for satisfiability in separation logic with inductive predicates, Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, p.15, 2013.
DOI : 10.1145/2603088.2603091

M. Barnett, K. Fähndrich, M. Rustan, P. Leino, W. Müller et al., Specification and verification, Communications of the ACM, vol.54, issue.6, pp.81-91, 2011.
DOI : 10.1145/1953122.1953145

[. Barnett, K. Rustan, M. Leino, and W. Schulte, The Spec# Programming System: An Overview, Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS), pp.49-69, 2004.
DOI : 10.1007/978-3-540-30569-9_3

J. Boyland, Checking Interference with Fractional Permissions, Static Analysis Symposium (SAS), volume 2694 of Lecture Notes in Computer Science, pp.55-72, 2003.
DOI : 10.1007/3-540-44898-5_4

[. Boyland, Semantics of fractional permissions with nesting, ACM Transactions on Programming Languages and Systems, vol.32, issue.6, 2010.
DOI : 10.1145/1749608.1749611

[. 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

[. Balabonski, F. Pottier, and J. Protzenko, Type Soundness and Race Freedom for Mezzo, Proceedings of the 12th International Symposium on Functional and Logic Programming, pp.253-269, 2014.
DOI : 10.1007/978-3-319-07151-0_16
URL : https://hal.archives-ouvertes.fr/hal-01081194

L. Birkedal, N. Rothwell, M. Tofte, and D. N. Turner, The ML kit (version 1), 1993.

W. Peter-canning, W. Cook, W. Hill, . Olthoff, C. John et al., F-bounded polymorphism for object-oriented programming, Proceedings of the fourth international conference on Functional programming languages and computer architecture, pp.273-280, 1989.

C. Calcagno, D. Distefano, P. W. Hearn, and H. Yang, Compositional shape analysis by means of bi-abduction, Principles of Programming Languages (POPL), pp.289-300, 2009.

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

. Cho-+-11-]-byron, C. Cook, J. Haase, M. Ouaknine, J. Parkinson et al., Tractable reasoning in a fragment of separation logic, CONCUR 2011?Concurrency Theory, pp.235-249, 2011.

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

A. Chlipala, G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky, Effective interactive proofs for higher-order imperative programs, International Conference on Functional Programming (ICFP), pp.79-90, 2009.

R. William and . Cook, Object-oriented programming versus abstract data types, Foundations of Object- Oriented Languages, pp.151-178, 1991.

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

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

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

[. Cardelli and P. Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys, vol.17, issue.4, pp.471-522, 1985.
DOI : 10.1145/6041.6042

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

[. Calcagno, H. Yang, W. Peter, and . O-'hearn, Computability and complexity results for a spatial assertion language for data structures Linear logic The Stanford Encyclopedia of Philosophy, In FST TCS Foundations of Software Technology and Theoretical Computer Science, pp.108-119, 2001.

R. Deline and M. Fähndrich, Enforcing high-level protocols in low-level software, Programming Language Design and Implementation (PLDI), pp.59-69, 2001.

R. Deline and M. Fähndrich, Typestates for Objects, European Conference on Object- Oriented Programming, pp.465-490, 2004.
DOI : 10.1007/978-3-540-24851-4_21

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

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.

J. Filliâtre, Why: a multi-language multi-prover verification tool, Research Report, vol.1366, 2003.

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

D. K. Gifford, P. Jouvelot, J. M. Lucassen, and M. A. Sheldon, FX-87 reference manual, 1987.

D. K. Gifford, P. Jouvelot, M. A. Sheldon, and J. W. Toole, Report on the FX-91 programming language, 1992.

D. Grossman, G. Morrisett, T. Jim, M. Hicks, Y. Wang et al., Region-based memory management in Cyclone, Programming Language Design and Implementation (PLDI), pp.282-293, 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. Guéneau, F. Pottier, and J. Protzenko, The ins and outs of iteration in Mezzo, 2013.

C. Haase, S. Ishtiaq, J. Ouaknine, J. Matthew, and . Parkinson, SeLoger: A Tool for Graph-Based Reasoning in Separation Logic, Computer Aided Verification, pp.790-795, 2013.
DOI : 10.1007/978-3-642-39799-8_55

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

R. Harper and B. C. Pierce, Design considerations for ML-style module systems, Advanced Topics in Types and Programming Languages, pp.293-345, 2005.

B. Jonas and . Jensen, Techniques for model construction in separation logic, 2013.

P. Jouvelot and D. Gifford, Algebraic reconstruction of types and effects, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '91, pp.303-310, 1991.
DOI : 10.1145/99583.99623

U. Juhasz, T. Ioannis, P. Kassios, M. Müller, M. Novacek et al., Viper: a verification infrastructure for permission-based reasoning, 2014.

T. Jim, G. Morrisett, D. Grossman, W. Michael, J. Hicks et al., Cyclone: A safe dialect of c, USENIX Annual Technical Conference, General Track, pp.275-288, 2002.

E. Donald and . Knuth, Structured programming with go to statements, ACM Computing Surveys (CSUR), vol.6, issue.4, pp.261-301, 1974.

C. Liang and D. Miller, Focusing and Polarization in Intuitionistic Logic, Computer Science Logic, pp.451-465, 2007.
DOI : 10.1007/978-3-540-74915-8_34
URL : https://hal.archives-ouvertes.fr/inria-00167231

[. Matsakis, PLT-redex model of rust, 2014.

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

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, 2011.
DOI : 10.1145/1929553.1929559

G. Morrisett, D. Walker, K. Crary, and N. Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems, vol.21, issue.3, pp.528-569, 1999.

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

C. Huu-hai-nguyen, S. David, W. Qin, and . Chin, Automated Verification of Shape and Size Properties Via Separation Logic, Verification, Model Checking and Abstract Interpretation (VMCAI), pp.251-266, 2007.
DOI : 10.1007/978-3-540-69738-1_18

U. Norell, Dependently typed programming in agda, Advanced Functional Programming, pp.230-266, 2009.

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.

[. Post, Real programmers don't use pascal, Datamation, vol.29, issue.7, 1983.

[. Pottier and D. Rémy, The essence of ML type inference, Advanced Topics in Types and Programming Languages, pp.389-489, 2005.

J. A. , N. Pérez, and A. Rybalchenko, Separation logic modulo theories, Programming Languages and Systems, pp.90-106, 2013.

C. John and . Reynolds, Three approaches to type structure, Theory and Practice of Software Development (TAPSOFT), pp.97-138, 1985.

C. John and . Reynolds, Separation logic: A logic for shared mutable data structures, Logic in Computer Science (LICS), pp.55-74, 2002.

[. Rival, Abstract Domains for the Static Analysis of Programs Manipulating Complex Data Structures . Habilitation à diriger des recherches, 2011.

D. Rémy, Type checking records and variants in a natural extension of ML, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '89, pp.77-88, 1989.
DOI : 10.1145/75277.75284

J. Swamy, C. Chen, P. Fournet, K. Strub, J. Bhargavan et al., Secure distributed programming with value-dependent types, International Conference on Functional Programming (ICFP), pp.266-278, 2011.
DOI : 10.1145/2034773.2034811
URL : https://hal.archives-ouvertes.fr/hal-00939188

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

J. Sunshine, K. Naden, S. Stork, J. Aldrich, and É. Tanter, First-class state change in plaid, ACM SIGPLAN Notices, vol.46, issue.10, pp.713-732, 2011.
DOI : 10.1145/2076021.2048122

G. Scherer and J. Protzenko, A toy type language: parsing and pretty-printing, 2014.

G. Scherer and J. Protzenko, A toy type language: using Fix to compute variance, 2014.

G. Scherer and J. Protzenko, A toy type language: variance 101, 2014.

F. Smith, D. Walker, and G. Morrisett, Alias Types, European Symposium on Programming (ESOP), volume 1782 of Lecture Notes in Computer Science, pp.366-381, 2000.
DOI : 10.1007/3-540-46425-5_24

E. Robert, S. Strom, and . Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, vol.12, issue.1, pp.157-171, 1986.

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.

J. A. Tov and R. Pucella, Stateful Contracts for Affine Types, European Symposium on Programming (ESOP), pp.550-569, 2010.
DOI : 10.1007/978-3-642-11957-6_29

[. 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

J. Tiuryn and P. Urzyczyn, The subtyping problem for second-order types is undecidable, Logic in Computer Science LICS'96. Proceedings., Eleventh Annual IEEE Symposium on, pp.74-85, 1996.

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

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

. Wikipedia, List of programming languages (alphabetical), 2014, 2014.

. Wikipedia, Singular they, 2014.

[. Walker and G. Morrisett, Alias Types for Recursive Data Structures, Types in Compilation (TIC), volume 2071 of Lecture Notes in Computer Science, pp.177-206, 2000.
DOI : 10.1007/3-540-45332-6_7