S. Abramsky, Computational interpretations of linear logic, Theoretical Computer Science, vol.111, issue.1-2, pp.1-2, 1993.
DOI : 10.1016/0304-3975(93)90181-R

B. Anderson, L. Bergstrom, M. Goregaokar, J. Matthews, K. Mcallister et al., Engineering the servo web browser engine using Rust, Proceedings of the 38th International Conference on Software Engineering Companion, ICSE '16, 2016.
DOI : 10.1145/2184489.2184508

R. Asati, A. Sanyal, A. Karkare, and A. Mycroft, Liveness-Based Garbage Collection Held as Part of the European Joint Conferences on Theory and Practice of Software, Compiler Construction -23rd International Conference Proceedings (Lecture Notes in Computer Science), pp.85-106, 2014.

D. F. Bacon, P. Cheng, and V. T. Rajan, A unified theory of garbage collection, Proceedings of the 19th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp.50-68, 2004.

G. Henry and . Baker, Linear logic and permutation stacks -the Forth shall be first. SIG- ARCH Computer Architecture News, pp.34-43, 1994.

G. Henry and . Baker, Minimum Reference Count Updating with Deferred and Anchored Pointers for Functional Data Structures, SIGPLAN Notices, vol.29, issue.52, pp.38-43, 1994.

G. Henry and . Baker, Use-Once" Variables and Linear Objects -Storage Management, Reflection and Multi-Threading, SIGPLAN Notices, vol.30, issue.53, pp.45-52, 1995.

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, p.54, 2016.
DOI : 10.1006/inco.1994.1093
URL : https://hal.archives-ouvertes.fr/hal-01246534

E. Barendsen and S. Smetsers, Uniqueness Typing for Functional Languages with Graph Rewriting Semantics, Mathematical Structures in Computer Science, vol.6, issue.6, pp.579-612, 1996.

N. Benton, M. Hofmann, and V. Nigam, Effect-dependent transformations for concurrent programs, Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, pp.188-201, 2016.
DOI : 10.1145/2967973.2968602
URL : http://arxiv.org/pdf/1510.02419

J. Berdine, W. Peter, . O-'hearn, S. Uday, H. Reddy et al., Linearly used continuations, Proceedings of the Third ACM SIGPLAN Workshop on Continuations (CW'01). Citeseer, pp.47-54, 2000.

J. Bernardy, M. Boespflug, R. R. Newton, S. P. Jones, and A. Spiwack, Linear Haskell: practical linearity in a higher-order polymorphic language, Proceedings of the ACM on Programming Languages, vol.2, issue.POPL, pp.1-5, 2018.
DOI : 10.1007/978-3-540-30557-6_8
URL : https://hal.archives-ouvertes.fr/hal-01673536

G. Bierman, What is a categorical model of Intuitionistic Linear Logic?, Proc. TLCA, pp.78-93, 1995.
DOI : 10.1007/BFb0014046

C. Maximilian, S. L. Bolingbroke, and . Jones, Types are calling conventions, Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell, pp.1-12, 2009.

J. Chirimar, C. A. Gunter, and J. G. Riecke, Abstract, Journal of Functional Programming, vol.21, issue.02, pp.195-244, 1996.
DOI : 10.1007/BFb0013458

D. Clarke and T. Wrigstad, External Uniqueness Is Unique Enough, ECOOP 2003 -Object-Oriented Programming, 17th European Conference, pp.176-200, 2003.
DOI : 10.1007/978-3-540-45070-2_9
URL : http://homepages.cwi.nl/~dave/writing/papers/euiue.pdf

D. G. Clarke, J. Potter, and J. Noble, Ownership Types for Flexible Alias Protection, Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA '98), pp.48-64, 1998.
DOI : 10.1145/286936.286947
URL : http://www.cs.uu.nl/~dave/papers/ownership.ps.gz

J. Clements, Portable and high-level access to the stack with Continuation Marks, Ph.D. Dissertation. Northeastern University, p.45, 2006.

J. Clements and M. Felleisen, A tail-recursive machine with stack inspection, ACM Transactions on Programming Languages and Systems, vol.26, issue.6, 2004.
DOI : 10.1145/1034774.1034778
URL : http://www.ccs.neu.edu/scheme/pubs/cf-toplas04.pdf

P. Curien, M. Fiore, and G. Munch-maccagnoni, A Theory of Effects and Resources: Adjunction Models and Polarised Calculi, Proc. POPL. https, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01256092

V. Danos, J. Joinet, and H. Schellinx, Abstract, The Journal of Symbolic Logic, vol.II, issue.03, pp.755-807, 1997.
DOI : 10.1007/BF00885763
URL : https://hal.archives-ouvertes.fr/inria-00528352

O. Danvy and L. R. Nielsen, CPS transformation of beta-redexes, Information Processing Letters, vol.94, issue.5, pp.217-224, 2005.
DOI : 10.1016/j.ipl.2005.02.002

S. Dolan, A. Sivaramakrishnan, and . Madhavapeddy, Bounding Data Races in Space and Time, Proc. PLDI, p.54, 2018.

A. Richard, S. P. Eisenberg, and . Jones, Levity polymorphism, Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, 2017.

M. Fähndrich and R. Deline, Adoption and Focus: Practical Linear Types for Imperative Programming, Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp.13-24, 2002.

M. Fluet, G. Morrisett, and A. J. Ahmed, Linear Regions Are All You Need Held as Part of the Joint European Conferences on Theory and Practice of Software, Programming Languages and Systems, 15th European Symposium on Programming Proceedings (Lecture Notes in Computer Science), Peter Sestoft, pp.7-21, 2006.

E. Gan, J. A. Tov, and G. Morrisett, Type Classes for Lightweight Substructural Types, Proceedings Third International Workshop on Linearity, pp.34-48, 2014.
DOI : 10.1145/292540.292545
URL : http://arxiv.org/pdf/1502.04772

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

J. Girard, A new constructive logic: classic logic, Mathematical Structures in Computer Science, vol.7, issue.2, pp.255-296, 1991.
DOI : 10.1016/0304-3975(87)90045-4

J. Girard, On the unity of logic, Annals of Pure and Applied Logic, vol.59, issue.3, pp.201-217, 1993.
DOI : 10.1016/0168-0072(93)90093-S
URL : https://hal.archives-ouvertes.fr/inria-00075095

T. G. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, pp.47-58, 1990.
DOI : 10.1145/96709.96714

D. Grossman, Quantified types in an imperative language, ACM Transactions on Programming Languages and Systems, vol.28, issue.3, 2006.
DOI : 10.1145/1133651.1133653

D. Grossman, J. G. Morrisett, T. Jim, M. W. Hicks, Y. Wang et al., Region-Based Memory Management in Cyclone, Proceedings of the, 2002.
DOI : 10.1145/512529.512563
URL : http://www.cs.cornell.edu/projects/cyclone/papers/cyclone-regions.pdf

E. Howard, P. Hinnant, D. Dimov, and . Abrahams, A Proposal to Add Move Semantics Support to the C++ Language, p.14, 2002.

M. Hofmann, A Type System for Bounded Space and Functional In-Place Update, 2000.

P. Gérard and . Huet, The Zipper, J. Funct. Program, vol.7, issue.5, pp.549-554, 1997.

T. Jim, J. G. Morrisett, D. Grossman, M. W. Hicks, J. Cheney et al., Cyclone: A Safe Dialect of C, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, pp.275-288, 2002.

R. Jung, J. Jourdan, R. Krebbers, and D. Dreyer, RustBelt: securing the foundations of the rust programming language, Proceedings of the ACM on Programming Languages, vol.2, issue.POPL, pp.1-66, 2018.
DOI : 10.1145/2500365.2500600
URL : https://hal.archives-ouvertes.fr/hal-01633165

N. Kobayashi, Quasi-linear types, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.29-42, 1999.
DOI : 10.1145/292540.292546

Y. Lafont, The linear abstract machine, Theoretical computer science, vol.59, issue.13, pp.1-2, 1988.
DOI : 10.1016/0304-3975(88)90100-4
URL : https://doi.org/10.1016/0304-3975(88)90100-4

J. Peter and . Landin, A Generalization of Jumps and Labels, Technical Report. Subsequently published as Landin, p.45, 1965.

J. Peter and . Landin, A Generalization of Jumps and Labels, Higher-Order and Symbolic Computation, pp.125-143, 1998.

X. Leroy, The ZINC experiment: an economical implementation of the ML language, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00070049

L. Paul-blain, Call-by-Push-Value: A Subsuming Paradigm, Proc. TLCA '99, pp.228-242, 1999.

L. Paul-blain, Call-By-Push-Value: A Functional/Imperative Synthesis, Semantic Structures in Computation, vol.2, issue.7, 2004.

P. Melliès, Categorical semantics of linear logic, Panoramas et Synthèses, vol.27, pp.15-215, 2009.

P. Melliès and N. Tabareau, Resource modalities in tensor logic, Annals of Pure and Applied Logic, vol.161, issue.5, pp.632-653, 2010.
DOI : 10.1016/j.apal.2009.07.018

H. Naftaly and . Minsky, Towards Alias-Free Pointers, ECOOP'96 -Object-Oriented Programming , 10th European Conference Proceedings (Lecture Notes in Computer Science), pp.189-209, 1996.

Y. Minsky, A. Madhavapeddy, and J. Hickey, Real World OCaml -Functional Programming for the Masses, 2013.

G. Morrisett, Compiling with Types, p.51, 1995.

G. Munch-maccagnoni, Formulae-as-types for an involutive negation, 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.45, 2014.
DOI : 10.1145/2603088.2603156
URL : https://hal.archives-ouvertes.fr/hal-00996742

W. Peter, J. O-'hearn, M. Power, R. D. Takeyama, and . Tennent, Syntactic Control of Interference Revisited, Theor. Comput. Sci, vol.228, pp.1-2, 1999.

F. Pottier and J. Protzenko, Programming with permissions in Mezzo, ACM SIGPLAN Notices, vol.48, issue.9, pp.173-184, 2013.
DOI : 10.1145/2544174.2500598
URL : https://hal.archives-ouvertes.fr/hal-00877590

R. Proust, ASAP: As Static as Possible memory management, 2016.

T. Ramananandro, G. D. Reis, and X. Leroy, A mechanized semantics for C++ object construction and destruction, with applications to resource management, ACM SIGPLAN Notices, vol.47, issue.1, pp.521-532, 2012.
DOI : 10.1145/2103621.2103718
URL : https://hal.archives-ouvertes.fr/hal-00674663

C. John and . Reynolds, Syntactic Control of Interference, Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pp.39-46, 1978.

R. Shi and H. Xi, A linear type system for multicore programming in ATS, Science of Computer Programming, vol.78, issue.8, 2013.
DOI : 10.1016/j.scico.2012.09.005

A. Spiwack, A dissection of L, 2014.

B. Stroustrup, The design and evolution of C++. Pearson Education India, 1994.

B. Stroustrup, Exception Safety: Concepts and Techniques, pp.60-76, 2001.
DOI : 10.1007/3-540-45407-1_4
URL : http://research.att.com/~bs/except.pdf

B. Stroustrup, H. Sutter, and G. Reis, A brief introduction to C++'s model for type-and resource-safety. (2015). https://github.com, p.16, 2015.

M. Tofte and L. Birkedal, A region inference algorithm, ACM Transactions on Programming Languages and Systems, vol.20, issue.4, pp.724-767, 1998.
DOI : 10.1145/291891.291894
URL : http://www.itu.dk/research/mlkit/kit_general/toplas98.ps.gz

M. Tofte and J. Talpin, Implementation of the Typed Call-by-Value lambda- Calculus using a Stack of Regions, Conference Record of POPL'94: 21st ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, pp.188-201, 1994.

J. A. Tov and R. Pucella, Practical affine types, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.447-458, 2011.
DOI : 10.1145/1925844.1926436

P. Wadler, Linear Types Can Change the World!, Programming Concepts and Methods, p.15, 1990.

D. Walker, Substructural type systems, Advanced Topics in Types and Programming Languages, pp.3-44, 2005.

D. Zhu and H. Xi, Safe Programming with Pointers Through Stateful Views, Practical Aspects of Declarative Languages, 7th International Symposium, PADL 2005 Proceedings (Lecture Notes in Computer Science), pp.83-97, 2005.
DOI : 10.1007/978-3-540-30557-6_8
URL : http://www.church-project.org/reports/electronic/./Zhu+Xi:PADL-2005.pdf.gz