By induction on the height of the judgments (the proof is the same as Stone-Harper's, except for cases LLL and EELLL ,
By induction hypothesis (4), G | = S(?) :: {} holds?)) by definition of the logical relation, (?)) holds ,
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 ,
Engineering formal metatheory, Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.3-15, 2008. ,
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
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
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
LNgen: Tool support for locally nameless representations ,
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
The Lambda-Calculus: its Syntax and Semantics, volume 103 of Studies in logic and the foundations of mathematics, 1984. ,
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
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
Syntactic logical relations for polymorphic and recursive types. Computation, Meaning and Logic, 2007. ,
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. ,
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
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
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
An applicative module calculus, Theory and Practice of Software Development 97, pp.622-636, 1997. ,
DOI : 10.1007/BFb0030630
Un calcul de modules pour les systèmes de types purs, Thèse de doctorat, 1998. ,
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
Sound and complete elimination of singleton kinds, ACM Transactions on Computational Logic, vol.8, issue.2, p.8, 2007. ,
DOI : 10.1145/1227839.1227840
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. ,
On understanding types, data abstraction, and polymorphism, ACM Computing Surveys, vol.17, issue.4, pp.471-523, 1985. ,
DOI : 10.1145/6041.6042
A type system for higher-order modules, Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, pp.236-249, 2003. ,
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
Mixin' up the ML module system, ICFP '08: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, pp.307-320, 2008. ,
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. ,
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
Understanding and Evolving the ML Module System, 2005. ,
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
A type system for recursive modules, Proceedings of ACM SIGPLAN International Conference on Functional Programming, pp.289-302, 2007. ,
The Calculi of Lambda-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages, 1987. ,
Modular object-oriented programming with units and mixins, ACM SIGPLAN International Conference on Functional Programming, 1998. ,
Units: Cool modules for hot languages, Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.236-248, 1998. ,
First-class modules and composable signatures in Objective Caml 3.12. Extended abstract, 2010. ,
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
Justifying Algorithms for ????-Conversion, FoSSaCS, pp.410-424, 2005. ,
DOI : 10.1007/978-3-540-31982-5_26
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
Type generativity in higher-order module systems, 2005. ,
Bounded existentials and minimal typing Circulated in manuscript form. Full version in Theoretical Computer Science, pp.75-96, 1992. ,
Proofs and types, 1989. ,
A framework for defining logics, Symposium on Logic in Computer Science, pp.194-204, 1987. ,
DOI : 10.1145/138027.138060
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
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
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
Design considerations for ML-style module systems, Advanced Topics in Types and Programming Languages, pp.293-345, 2005. ,
A type-theoretic interpretation of Standard ML, Proof, Language, and Interaction: Essays in Honor of Robin Milner, 2000. ,
Abstract, Journal of Functional Programming, vol.700, issue.02, pp.135-154, 1995. ,
DOI : 10.1016/0022-4049(88)90124-7
Resource operators for lambda-calculus. Information and Computation, pp.419-473, 2007. ,
URL : https://hal.archives-ouvertes.fr/hal-00148539
Towards a mechanized metatheory of Standard ML, SIGPLAN Not, vol.42, issue.1, pp.173-184, 2007. ,
Didier Rémy, and Jérôme Vouillon. The Objective Caml system release 3, 2010. ,
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
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
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
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
Translucent Sums: A Foundation for Higher-Order Module Systems, 1997. ,
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
Réductions correctes et optimales dans le lambda-calcul, Thèse d'état, 1978. ,
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
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
Representation independence and data abstraction, POPL '86: Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp.263-276, 1986. ,
On the equivalence of data representations Artificial intelligence and mathematical theory of computation: papers in honor of John McCarthy, pp.305-329, 1991. ,
Experience report: Mechanizing core F-zip using the locally nameless approach, Presented at the 5th ACM SIGPLAN Workshop on Mechanizing Metatheory, 2010. ,
Abstract types have existential type, ACM Trans. Program. Lang. Syst, vol.10, issue.3, pp.470-502, 1988. ,
Modeling abstract types in modules with open existential types, Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, 2009. ,
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. ,
The Definition of Standard ML (Revised), 1997. ,
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
Implementing the TILT internal language, 2001. ,
Types abstraits dans les systèmes répartis, 2008. ,
Twelf User's Guide, 2002. ,
Types, abstraction and parametric polymorphism, Information Processing 83, pp.513-523, 1983. ,
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
F-ing modules, ACM SIGPLAN Workshop on Types in Language Design and Implementation, 2010. ,
Types for Modules, Electronic Notes in Theoretical Computer Science, vol.60, 1998. ,
DOI : 10.1016/S1571-0661(05)82621-0
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
Recursive structures for Standard ML, Proceedings of the 2001 ACM SIGPLAN International Conference on Functional Programming, pp.50-61, 2001. ,
Types for Modules, Electronic Notes in Theoretical Computer Science, vol.60, 2003. ,
DOI : 10.1016/S1571-0661(05)82621-0
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
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. ,
Typed cross-module compilation, ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming, pp.141-152, 1998. ,
Transparent modules with fully syntatic signatures, ICFP '99: Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, pp.220-232, 1999. ,
Ott: Effective tool support for the working semanticist, JFP, vol.20, issue.1, pp.71-122, 2010. ,
A bisimulation for dynamic sealing, POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.161-172, 2004. ,
Equational theories with recursive types. Under consideration for publication in, Journal Functional Programming ,
Singleton Types and Singleton Kinds, 2000. ,
Type definitions, Advanced Topics in Types and Programming Languages, pp.347-385, 2005. ,
Parallel reductions in ?-calculus. Information and Computation, pp.120-127, 1995. ,
Confluence by decreasing diagrams, converted, Proceedings of the 19th RTA, pp.306-320, 2008. ,
A syntactic approach to type soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994. ,
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