A. Abel, MiniAgda: Integrating Sized and Dependent Types, Workshop on Partiality And Recursion in Interactive Theorem Provers (PAR), 2010.
DOI : 10.4204/EPTCS.43.2

T. Altenkirch, N. A. Danielsson, A. Löh, and N. Oury, ????: Dependent Types without the Sugar, Functional and Logic Programming, pp.40-55, 2010.
DOI : 10.1007/978-3-642-12251-4_5

M. Roberto, L. Amadio, and . Cardelli, Subtyping recursive types, ACM Transactions on Programming Languages and Systems, vol.15, issue.4, pp.575-631, 1993.

A. W. Appel, C. D. Paul-andrémellì-es, J. Richards, and . Vouillon, A very modal model of a modern, major, general type system, ACM Symposium on Principles of Programming Languages (POPL), pp.109-122, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00150978

R. Atkey, Parameterised notions of computation, Journal of Functional Programming, vol.22, issue.3-4, pp.3-4355, 2009.
DOI : 10.1145/158511.158524

P. Henk and . Barendregt, The Lambda Calculus, Its Syntax and Semantics, 1984.

L. Birkedal, J. Schwinghammer, and K. Støvring, A metric model of lambda calculus with guarded recursion, 2010.

L. Birkedal, K. Støvring, and J. Thamsborg, The categorytheoretic solution of recursive metric-space quations, 2009.

L. Birkedal, K. Støvring, and J. Thamsborg, Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types, Mathematical Structures in Computer Science, vol.11, issue.4, 2010.
DOI : 10.1137/0211062

M. Brandt and F. Henglein, Coinductive axiomatization of recursive type equality and subtyping, Fundamenta Informaticae, vol.33, pp.309-338, 1998.
DOI : 10.1007/3-540-62688-3_29

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

R. Harper, A simplified account of polymorphic references, Information Processing Letters, vol.51, issue.4, pp.201-206, 1994.
DOI : 10.1016/0020-0190(94)90120-1

A. Hobor, R. Dockins, and A. W. Appel, A theory of indirection via approximation, ACM Symposium on Principles of Programming Languages (POPL), 2010.

B. Soren and . Lassen, Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context, Mathematical Foundations of Programming Semantics, pp.346-374, 1999.

L. Paul-blain, Possible world semantics for general storage in callby-value, Computer Science Logic, 2002.

C. John and . Mitchell, Polymorphic type inference and containment. Information and Computation, pp.211-249, 1988.

E. Moggi, Notions of computation and monads. Information and Computation, 1991.

E. Moggi and A. Sabry, An abstract monadic semantics for value recursion, Informatique théorique et applications, pp.377-400, 2004.
DOI : 10.1051/ita:2004018

R. Ejlers, M. , and S. Staton, Full abstraction in a metalanguage for state, Workshop on Syntax and Semantics of Low Level Languages, 2010.

H. Nakano, A modality for recursion, Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332), pp.255-266, 2000.
DOI : 10.1109/LICS.2000.855774

H. Nakano, Fixed-Point Logic with the Approximation Modality and Its Kripke Completeness, International Symposium on Theoretical Aspects of Computer Software (TACS), pp.165-182, 2001.
DOI : 10.1007/3-540-45500-0_8

A. Nanevski, G. Morrisett, and L. Birkedal, Hoare type theory, polymorphism and separation, Journal of Functional Programming, vol.18, pp.5-6, 2008.

W. O. Peter, J. C. Hearn, and . Reynolds, From Algol to polymorphic linear lambda-calculus, Journal of the ACM, vol.47, issue.1, pp.167-223, 2000.

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

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, A formalization of Nakano's type system. http: //gallium.inria.fr, 2009.

F. Pottier, The electronic FORK, 2010.

F. Pottier, A typed store-passing translation for general references (extended version), 2010.

J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang, Nested Hoare Triples and Frame Rules for Higher-Order Store, Computer Science Logic, 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, International Conference on Foundations of Software Science and Computation Structures (FOSSACS), pp.2-17, 2010.
DOI : 10.1007/978-3-642-12032-9_2

C. Strachey, Fundamental concepts in programming languages . Higher-Order and Symbolic Computation, pp.11-49, 2000.

M. Takahashi, Parallel reductions in ?-calculus. Information and Computation, pp.120-127, 1995.

D. Robert, D. Tennent, and . Ghica, Abstract models of storage. Higher-Order and Symbolic Computation, pp.119-129, 2000.

K. Andrew, M. Wright, and . Felleisen, A syntactic approach to type soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994.