. Proof, By induction on the height of the judgments (the proof is the same as Stone-Harper's, except for cases LLL and EELLL

@. Wwkkkksss, By induction hypothesis (4), G | = S(?) :: {} holds?)) by definition of the logical relation, (?)) holds

@. Wwkkkkpp, We have ?, ?::? 1 HS ? 2 ok, therefore there is a strict sub-derivation ? HS ? 1 ok. Hence, by induction hypothesis (1) we have G | = S(? 1 ) Now let G G and assume G | = T 1 :: S(? 1 ) Let S = S, ? ? T 1 . By Lemma 3.5.30 on page 87 and Lemma 3.5.36, G | = S : ?, ? :: ? 1 holds. Then, by induction hypothesis (1), we get G | = S (? 2 ), Since ? / ? fv(S), S (? 2 ) = S(? 2 )[? ? T 1 ]. Hence G | = S(? 2 )[? ? T 1 ]. Therefore, by definition of the logical relation, G | = S(?(? : ? 1 ) ? 2 ) holds

A. Acp-+-08-]-brian-aydemir, B. C. Charguéraud, R. Pierce, S. Pollack, and . Weirich, Engineering formal metatheory, Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.3-15, 2008.

M. Abadi, G. Gonthier, and B. Werner, Choice in Dynamic Linking, FOSSACS'04 -Foundations of Software Science and Computation Structures, pp.12-26, 2004.
DOI : 10.1007/978-3-540-24727-2_3

Y. Akama, On Mints' reduction for ccc-calculus, TLCA '93: Proceedings of the International Conference on Typed Lambda Calculi and Applications, pp.1-12, 1993.
DOI : 10.1007/BFb0037094

D. Aspinall, Subtyping with singleton types, Eighth International Workshop on Computer Science Logic, pp.1-15, 1995.
DOI : 10.1007/BFb0022243
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.5450

B. Aydemir and S. Weirich, LNgen: Tool support for locally nameless representations

E. [. Ancona and . Zucca, A theory of mixin modules: basic and derived operators, Mathematical Structures in Computer Science, vol.8, issue.4, pp.401-446, 1998.
DOI : 10.1017/S0960129598002576

]. H. Bar84 and . Barendregt, The Lambda-Calculus: its Syntax and Semantics, volume 103 of Studies in logic and the foundations of mathematics, 1984.

G. Boudol, The recursive record semantics of objects revisited, Journal of functional Programming, vol.14, issue.3, pp.263-315, 2004.
DOI : 10.1017/S0956796803004775
URL : https://hal.archives-ouvertes.fr/inria-00072423

P. Curien, R. D. , and C. , Abstract, Journal of Functional Programming, vol.27, issue.02, pp.299-327, 1996.
DOI : 10.1007/BFb0037094
URL : https://hal.archives-ouvertes.fr/hal-00155295

K. Crary and R. Harper, Syntactic logical relations for polymorphic and recursive types. Computation, Meaning and Logic, 2007.

R. Di, C. , and D. Kesner, A confluent reduction for the extensional typed lambda-calculus with pairs, sums, recursion and terminal object, Intern. Conf. on Automata, Languages and Programming (ICALP), pp.645-656, 1993.

[. Cardelli and X. Leroy, Abstract types and the dot notation, Proceedings IFIP TC2 working conference on programming concepts and methods, pp.479-504, 1990.
URL : https://hal.archives-ouvertes.fr/hal-01499980

R. L. Constable, Recent Results in Type Theory and Their Relationship to Automath, Thirty Five Years of Automating Mathematics, pp.1-11, 2003.
DOI : 10.1007/978-94-017-0253-9_3

[. Cosmo, On the power of simple diagrams, RTA '96: Proceedings of the 7th International Conference on Rewriting Techniques and Applications, pp.200-214, 1996.
DOI : 10.1007/3-540-61464-8_53

J. Courant, An applicative module calculus, Theory and Practice of Software Development 97, pp.622-636, 1997.
DOI : 10.1007/BFb0030630

J. Courant, Un calcul de modules pour les systèmes de types purs, Thèse de doctorat, 1998.

J. Courant, Strong Normalization with Singleton Types, ITRS '02, Intersection Types and Related Systems (FLoC Satellite Event), pp.53-71, 2003.
DOI : 10.1016/S1571-0661(04)80490-0

K. Crary, Sound and complete elimination of singleton kinds, ACM Transactions on Computational Logic, vol.8, issue.2, p.8, 2007.
DOI : 10.1145/1227839.1227840

K. Crary, A syntactic account of singleton types via hereditary substitution Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, cS06] Chung chieh Shan. Higher-order modules in System F-omega and Haskell. Draft, 2006.

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

[. Dreyer, K. Crary, and R. Harper, A type system for higher-order modules, Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, pp.236-249, 2003.

[. Cosmo and D. Kesner, Simulating expansions without expansions, Mathematical Structures in Computer Science, vol.27, issue.03, 1911.
DOI : 10.1305/ndjfl/1093883461
URL : https://hal.archives-ouvertes.fr/inria-00074762

D. Dreyer and A. Rossberg, Mixin' up the ML module system, ICFP '08: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, pp.307-320, 2008.

D. Dreyer, A type system for well-founded recursion, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '04, pp.293-305, 2004.

D. Dreyer, Recursive type generativity, Proceedings of ACM SIGPLAN International Conference on Functional Programming, pp.41-53, 2005.
DOI : 10.1145/1086365.1086372
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.137.1114

D. Dreyer, Understanding and Evolving the ML Module System, 2005.

D. Dreyer, Recursive type generativity, Journal of Functional Programming, pp.433-471, 2007.
DOI : 10.1145/1086365.1086372
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.137.1114

D. Dreyer, A type system for recursive modules, Proceedings of ACM SIGPLAN International Conference on Functional Programming, pp.289-302, 2007.

[. Felleisen, The Calculi of Lambda-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages, 1987.

R. Bruce, F. , and M. Flatt, Modular object-oriented programming with units and mixins, ACM SIGPLAN International Conference on Functional Programming, 1998.

M. Flatt and M. Felleisen, Units: Cool modules for hot languages, Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.236-248, 1998.

A. Frisch and J. Garrigue, First-class modules and composable signatures in Objective Caml 3.12. Extended abstract, 2010.

D. Grossman, G. Morrisett, and S. Zdancewic, Syntactic type abstraction, ACM Transactions on Programming Languages and Systems, vol.22, issue.6, pp.1037-1080, 2000.
DOI : 10.1145/371880.371887
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.2708

H. Goguen, Justifying Algorithms for ????-Conversion, FoSSaCS, pp.410-424, 2005.
DOI : 10.1007/978-3-540-31982-5_26

H. Goguen, A syntactic approach to eta equality in type theory, ACM SIGPLAN Notices, vol.40, issue.1, pp.75-84, 2005.
DOI : 10.1145/1047659.1040312

P. Govereau, Type generativity in higher-order module systems, 2005.

G. Ghelli and B. Pierce, Bounded existentials and minimal typing Circulated in manuscript form. Full version in Theoretical Computer Science, pp.75-96, 1992.

[. Girard, P. Taylor, and Y. Lafont, Proofs and types, 1989.

[. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Symposium on Logic in Computer Science, pp.194-204, 1987.
DOI : 10.1145/138027.138060

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

M. Hofmann and B. C. Pierce, Type Destructors, Informal proceedings of the Fourth International Workshop on Foundations of Object-Oriented Languages (FOOL), 1998.
DOI : 10.1006/inco.2001.2926
URL : http://doi.org/10.1006/inco.2001.2926

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

R. Harper and C. Stone, A type-theoretic interpretation of Standard ML, Proof, Language, and Interaction: Essays in Honor of Robin Milner, 2000.

[. Jay and N. Ghani, Abstract, Journal of Functional Programming, vol.700, issue.02, pp.135-154, 1995.
DOI : 10.1016/0022-4049(88)90124-7

D. Kesner and S. Lengrand, Resource operators for lambda-calculus. Information and Computation, pp.419-473, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00148539

K. Daniel, K. Lee, R. Crary, and . Harper, Towards a mechanized metatheory of Standard ML, SIGPLAN Not, vol.42, issue.1, pp.173-184, 2007.

X. Leroy, D. Doligez, and J. Garrigue, Didier Rémy, and Jérôme Vouillon. The Objective Caml system release 3, 2010.

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

X. Leroy, Abstract, Journal of Functional Programming, vol.6, issue.05, pp.667-698, 1996.
DOI : 10.1017/S0956796800001933
URL : https://hal.archives-ouvertes.fr/hal-01499980

X. Leroy, A modular module system, Journal of Functional Programming, vol.10, issue.3, pp.269-303, 2000.
DOI : 10.1017/S0956796800003683
URL : https://hal.archives-ouvertes.fr/inria-00073825

[. Lillibridge, Translucent Sums: A Foundation for Higher-Order Module Systems, 1997.

J. J. Leifer, G. Peskine, P. Sewell, and K. Wansbrough, Global abstraction-safe marshalling with hash types, ACM SIGPLAN Notices, vol.38, issue.9, pp.87-98, 2003.
DOI : 10.1145/944746.944714
URL : https://hal.archives-ouvertes.fr/inria-00071732

J. Lévy, Réductions correctes et optimales dans le lambda-calcul, Thèse d'état, 1978.

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

C. John and . Mitchell, Representation independence and data abstraction, POPL '86: Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp.263-276, 1986.

C. John and . Mitchell, On the equivalence of data representations Artificial intelligence and mathematical theory of computation: papers in honor of John McCarthy, pp.305-329, 1991.

B. Montagu, Experience report: Mechanizing core F-zip using the locally nameless approach, Presented at the 5th ACM SIGPLAN Workshop on Mechanizing Metatheory, 2010.

C. John, G. D. Mitchell, and . Plotkin, Abstract types have existential type, ACM Trans. Program. Lang. Syst, vol.10, issue.3, pp.470-502, 1988.

[. Montagu and D. Rémy, Modeling abstract types in modules with open existential types, Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, 2009.

[. Montagu and D. Rémy, Types abstraits et types existentiels ouverts, Actes des deuxièmes journées nationales du Groupement De Recherche CNRS du Génie de la Programmation et du Logiciel, pp.147-148, 2010.

[. Milner, M. Tofte, R. Harper, and D. Macqueen, The Definition of Standard ML (Revised), 1997.

M. Odersky, V. Cremet, C. Röckl, and M. Zenger, A Nominal Theory of Objects with Dependent Types, Proceedings of European Conference on Object- Oriented Programming, pp.201-224, 2003.
DOI : 10.1007/978-3-540-45070-2_10

L. Petersen, P. Cheng, R. Harper, and C. Stone, Implementing the TILT internal language, 2001.

G. Peskine, Types abstraits dans les systèmes répartis, 2008.

F. Pfenning and C. Schuermann, Twelf User's Guide, 2002.

C. John and . Reynolds, Types, abstraction and parametric polymorphism, Information Processing 83, pp.513-523, 1983.

A. Rossberg, Generativity and dynamic opacity for abstract types, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming , PPDP '03, pp.241-252, 2003.
DOI : 10.1145/888251.888274

[. Rossberg, C. V. Russo, and D. Dreyer, F-ing modules, ACM SIGPLAN Workshop on Types in Language Design and Implementation, 2010.

C. V. Russo, Types for Modules, Electronic Notes in Theoretical Computer Science, vol.60, 1998.
DOI : 10.1016/S1571-0661(05)82621-0

C. V. Russo, Non-dependent Types for Standard ML Modules, Proceedings of ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp.80-97, 1999.
DOI : 10.1007/10704567_5

C. V. Russo, Recursive structures for Standard ML, Proceedings of the 2001 ACM SIGPLAN International Conference on Functional Programming, pp.50-61, 2001.

C. V. Russo, Types for Modules, Electronic Notes in Theoretical Computer Science, vol.60, 2003.
DOI : 10.1016/S1571-0661(05)82621-0

M. Sulzmann, M. M. Chakravarty, S. P. Jones, and K. Donnelly, System F with type equality coercions, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation , TLDI '07, pp.53-66, 2007.
DOI : 10.1145/1190315.1190324

A. Christopher, R. Stone, and . Harper, Deciding type equivalence in a language with singleton kinds, POPL '00: Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.214-227, 2000.

Z. Shao, Typed cross-module compilation, ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming, pp.141-152, 1998.

Z. Shao, Transparent modules with fully syntatic signatures, ICFP '99: Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, pp.220-232, 1999.

P. Sewell, F. Z. Nardelli, S. Owens, G. Peskine, T. Ridge et al., Ott: Effective tool support for the working semanticist, JFP, vol.20, issue.1, pp.71-122, 2010.

[. Sumii and B. C. Pierce, A bisimulation for dynamic sealing, POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.161-172, 2004.

A. Ss-]-christopher, A. P. Stone, and . Schoonmaker, Equational theories with recursive types. Under consideration for publication in, Journal Functional Programming

A. Christopher and . Stone, Singleton Types and Singleton Kinds, 2000.

A. Christopher and . Stone, Type definitions, Advanced Topics in Types and Programming Languages, pp.347-385, 2005.

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

. Vincent-van-oostrom, Confluence by decreasing diagrams, converted, Proceedings of the 19th RTA, pp.306-320, 2008.

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

R. [. Wells and . Vestergaard, Equational Reasoning for Linking with First-Class Primitive Modules, ESOP '00: Proceedings of the 9th European Symposium on Programming Languages and Systems, pp.412-428, 2000.
DOI : 10.1007/3-540-46425-5_27