S. If, end, then [T {t j ? p.t, x k ? p.x | t j ? BV

S. If, structure x i : S ; D 2 end, then [S {t j ? p.t, x k ? p.x | t j ? BV

?. Since, Hence S is of the format sig D 1 ; structure x i : S ; D 2 end Applying rule 20, we obtain E p : S where S = S {t j ? q.t, x k ? q.x | t j ? BV (D 1 ), x k ? BV (D 1 )}. Moreover, it follows from (3) that [S] ? = ?(q.x) = ?(p) For the " only if " part, assume E p : S. Then, by rule 20, E q : S and S = sig D 1 ; structure x i : S ; D 2 end, with S = S {t j ? q.t, x k ? q, BV (D 1 ), x k ? BV (D 1 )}. Applying the induction hypothesis, we get that ?(q) is defined and [S ] ? = ?(q). Since S contains a field named x, ?(p) is defined as well, and (3) implies ?(p) = [S] ?

?. Since, S 1 )S 2 ] ? , there exists a substitution ? such that Dom(?) ? F S(? 1 ) \ F S(?) and ? 1 = ?(? 1 ) and ? 2 = ?(? 2 ). (We have assumed) without loss of generality, since the condition N ? F S(?) = ? is met.) Applying the induction hypothesis to ? p ? ? p , we get a signature expression S p such that E p : S p and, proposition 11 shows that E S p <: S 1 . We can therefore apply rule 22, obtaining E f i (p) : S 2 {x i ? p}. By proposition 12, we get the expected result [S 2 {x i ? s}] ? = ? ?(? 2 ) = ?

C. , =. , ?. {t-i, ?. , }. et al., By proposition 6, we have ? = [T ] ? . Therefore, [E; type t i = T ] = ? + {t i ? ? }. Applying the induction hypothesis to d , we obtain D such that E; type t i = T d : D and [D ] ? = ? ? , where ? is ? + {t i ? ? }. Moreover, BV (E) follows from the hypothesis t i / ? Dom(?). By rule 25

=. Case-d, Same proof as in the previous case. The condition n / ? F S(?) in rule 8' ensures that

=. Case-d, By rule 10', ? s ? ? 1 and Dom(? 1 ) ? Dom(?) = ? and ?+? 1 d ? ? 2 and ? = ? 1 +? 2 . By induction hypothesis, we have E s : S 1 for some signature expression S 1 such that

M. Aponte, Extending record typing to type parametric modules with sharing, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '93, pp.465-478, 1993.
DOI : 10.1145/158511.158704
URL : https://hal.archives-ouvertes.fr/inria-00074768

L. Cardelli, Typeful programming, Formal description of programming concepts, pp.431-507, 1989.

L. Cardelli and X. Leroy, Abstract types and the dot notation, Proceedings IFIP TC2 working conference on programming concepts and methods North-Holland. Also available as research report 56, pp.479-504, 1990.
URL : https://hal.archives-ouvertes.fr/hal-01499980

L. Cardelli and D. B. Macqueen, Persistence and Type Abstraction, Data types and persistence, 1988.
DOI : 10.1007/978-3-642-61556-6_3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.97.3858

L. Cardelli and P. Wegner, On understanding types, data abstraction, and polymorphism . Computing surveys, pp.471-522, 1985.
DOI : 10.1145/6041.6042
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.117.695

G. Gran, An error in rule 55 of the definition of Standard ML, 1995.

R. Harper and M. Lillibridge, A type-theoretic approach to higher-order modules with sharing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '94, pp.123-137, 1994.
DOI : 10.1145/174675.176927

R. Harper, R. Milner, and M. Tofte, A type discipline for program modules, Lecture Notes in Computer Science, vol.87, issue.250, pp.308-319, 1987.
DOI : 10.1007/BFb0014988

R. Harper and J. C. Mitchell, On the type structure of standard ML, ACM Transactions on Programming Languages and Systems, vol.15, issue.2, pp.211-252, 1993.
DOI : 10.1145/169701.169696

R. Harper, J. C. Mitchell, and E. Moggi, Higher-order modules and the phase distinction, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, pp.341-354, 1990.
DOI : 10.1145/96709.96744
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.3795

X. Leroy, Manifest types, modules, and separate compilation, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '94, pp.109-122, 1994.
DOI : 10.1145/174675.176926
URL : https://hal.archives-ouvertes.fr/hal-01499976

X. Leroy, Applicative functors and fully transparent higher-order modules, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '95, pp.142-153, 1995.
DOI : 10.1145/199448.199476
URL : https://hal.archives-ouvertes.fr/hal-01499966

B. Liskov and J. Guttag, Abstraction and specification in program development, 1986.

D. B. Macqueen, Modules for standard ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming , LFP '84, pp.198-207, 1984.
DOI : 10.1145/800055.802036

D. B. Macqueen, Using dependent types to express modular structure, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '86, pp.277-286, 1986.
DOI : 10.1145/512644.512670

D. B. Macqueen and M. Tofte, A semantics for higher-order functors, Programming languages and systems ? ESOP '94, pp.409-423, 1994.
DOI : 10.1007/3-540-57880-3_27

R. Milner and M. Tofte, Commentary on Standard ML, 1991.

R. Milner, M. Tofte, and R. Harper, The definition of Standard ML, 1990.

J. C. Mitchell and G. D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems, vol.10, issue.3, pp.470-502, 1988.
DOI : 10.1145/44501.45065

C. Russo, Generativity of names in the static semantics of Standard ML, 1995.

A. Sabry and M. Felleisen, Reasoning about programs in continuation-passing style, Lisp and Functional Programming 1992, pp.288-298, 1992.
DOI : 10.1007/bf01019462
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.122.1481

M. Tofte, Operational semantics and polymorphic type inference, 1988.

M. Tofte, Principal signatures for higher-order program modules, 19th symposium Principles of Programming Languages, pp.189-199, 1992.
DOI : 10.1145/143165.143206
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.1425

N. Wirth, Programming in Modula-2, 1983.
DOI : 10.1007/978-3-642-96878-5