I. Lemma, 3 (a purely abstract suffix does not change the substitution) If E 1 is a purely abstract environment then partenvsub E0, pp.1-1

. Proof, Trivial from Definition I.2 (partial type substitution associated to an environment)

I. Lemma, 4 (stability of types through revelation) If E hm T :Type then E hm reveal hm T :Type and E hm T == reveal hm T and E hm partenvsub E T :Type and E hm T == partenvsub E T . A trivial consequence that we also use is that if E hm T :Type then E hm reveal hm partenvsub E T :Type and E hm T ==

I. E. Lemma, X. ==-t-or, E. , and T. ==-x, Eq(T ) or E hm T :Eq(X ) or E hm, Also, if E is purely abstract, then E hm U :[Y :Eq(X ), T ] cannot be derived

B. Lemma and G. , 4 (discreteness of subkinding below Type) and reversing (Keq.Eq), there exists T 1 such that K = Eq(T 1 ) and E hm T 1 == T by a subproof. By induction on the subproof of E hm X :Eq(T 1 ), we get T 1 = X . Since E hm X == T by a subproof

T. Case, Eq(X ): There exists K such that the premises are E hm T :K and E hm K <: Eq(X )

B. Lemma and G. , 4 (discreteness of subkinding below Type) and reversing (Keq.Eq), there exists T 1 such that K = Eq(T 1 ) and E hm T 1 == X by a subproof. By induction, we get T 1 = X . Since E hm T :Eq(X ) by a subproof

. Case and . Teq, tran): Then by induction the " middle type " is X , whence by induction again T = X

E. Case, {. Type?z, and . }t, Then partenvsub E = partenvsub E0 {U .TYPE?T 0 }. Let Z be a fresh variable, and let E = E 0 , Z :Eq(T 0 ), {U .TYPE?Z }E 1 . By the definition of partenvsub, we have partenvsub E = partenvsub E0 {Z ?T 0 }. Since Z is fresh

B. Lemma and F. , 31 (type preservation by module substitution in coloured judgements for type world judgements), since E hm T :Type, we get E hm {U .TYPE?Z }T :Type. Similarly we have E hm {U, TYPE?Z }T :Type. By the previous case

I. Theorem, 7 (semantic interpretation of type world judgements) Let E hm J be any type world judgement. It is derivable iff all of the following conditions are met: 1. E has no repetition in the domain and unresolved free variables. 2. All the free variables of J are

E. Case and . Ok, Type or T hm S ok: no extra condition

E. Case and K. , K : either K = Type, or there exist T and T such that

E. Case, U. , and T. , E contains a binding of the form U :[X :K 1 , T 2 ] for some K 1 and T 2 , and E hm

. Proof, E. If, and J. , 6 (environments have to be ok) and Lemma E.8 (ok environments have no repetition in the domain) and Lemma F.13 (ok environments have no unresolved free variables); all the hashes in J are correct by Lemma E.5 (hashes have to be ok), and all the free variables of J are in dom E by Lemma E.9 (free variables of a judgement come from the environment)

E. Cases, . Ok, and . Type, Since there is no extra condition, we just have to prove that the judgement is derivable

E. Case, Given the (envok.*) rules, this judgement is derivable iff the judgement E hm ?:? is. By induction

E. Case and T. , Type: By the previous cases, E hm ok is derivable. By Lemma F.9 (types are ok provided their hashes are)

C. =. If and N. U. , [X :Type, T ] in CL is correct then ?CL is correct where ? = {U .TYPE?h, U .term?[v ? ] {X ?h}T h } and h = hash

. B. Proof and . Lemma, machine judgement characterisation of correct multiple-let contexts), the hypotheses are equivalent to nil ? CL():UNIT and the conclusions are equivalent to nil ? ?CL ():UNIT. By the definition of machine reduction CL() ?? ? ?CL () in both cases. By Theorem G.18 (type preservation for machine reduction, we get nil ? ?CL ():UNIT, as desired

=. Each-hash-in-?t-i and . {u, TYPE?T }T i is an element of the union of the hashes in T and T i , which is disjoint from hashlistofcl CL = hashlistofcl CL by hypotheses 3

.. E. Lem, 3 non-membership in domain is interpreted trivially, p.35

O. Lem, 7 prefixes of ok environments, p.35

.. E. Lem, 8 ok environments have no repetition in the domain, p.35

.. E. Lem, 9 free variables of a judgement come from the environment, p.36

.. E. Def, 11 type world judgement, p.37

.. E. Def, 12 hashes in something, p.37

.. E. Def, 13 partial order on colours, p.37

. E. Def and .. Pvu, 15 alternate, informal definition of, p.37

.. E. Lem, 18 stability of values by substitution, p.38

.. E. Lem, 19 computing the pvu of a type world judgement, p.38

F. Lem, 20 connection between fv, p.39

.. E. Lem, 21 types do not contain free expression variables, p.39

.. E. Lem, 22 environments do not contain free expression variables, p.39

.. E. Lem, 23 expression substitution in environment, p.39

.. F. Lem, 1 " type of a machine " judgements are not used to prove other coloured judgements, p.39

.. F. Lem, 2 colour stripping judgements, p.39

.. F. Lem, 4 merging environments, p.41

.. F. Lem, 6 kinds are smaller than Type, p.41

.. F. Lem, 7 relating type-is-kind and subkinding, p.42

.. F. Lem, 9 types are ok provided their hashes are, p.42

.. F. Lem, 10 colour change preserves type okedness, p.42

.. F. Def, 11 unresolved free variables of an environment, p.42

.. F. Lem, 12 computing unresolved free variables, p.42

.. F. Lem, 13 ok environments have no unresolved free variables, p.43

.. F. Lem, 14 type preservation by substitution, p.43

.. F. Def, 16 visible type-part of a module, p.44

.. F. Def, 17 visible term-part of a module, p.45

.. F. Def, 18 set of equations used to type a module, p.45

.. F. Lem, 19 reflexivity of kind equivalence, p.45

.. F. Lem, 20 weakening kind to ok kind in the environment, p.45

.. F. Lem, 21 things have to be ok, p.45

.. F. Lem, 22 weakening kind in the environment, p.47

.. F. Lem, 23 type preservation by guarded expression variable substitution, p.47

.. F. Lem, 24 type equivalence is a congruence, p.47

.. F. Lem, 25 type substitution in equivalence, p.48

.. F. Lem, 26 reversing subsignaturing judgement, p.48

.. F. Lem, 27 reversing module value variable typing judgement, p.48

.. F. Lem, 28 obtaining module value variable typing judgement, p.48

.. F. Lem, 29 type preservation by module substitution in coloured judgements, p.49

.. F. Lem, 30 type world judgements do not contain free expression variables, p.51

. Lem, 31 type preservation by module substitution in coloured judgements for type world judgements, p.51

.. F. Lem, 32 simplified module and type equality substitution for type world judgements, p.51

.. F. Lem, 33 type preservation by fully carried out module substitution, p.51

.. G. Lem, 1 shortening typing proof, p.52

.. G. Lem, 2 reversing typing proof through a context, p.52

.. G. Lem, 3 transitivity of kind equivalence, p.52

.. G. Lem, 4 discreteness of subkinding below Type, p.53

.. G. Lem, 7 signature rewriting in a type world judgement, p.53

.. G. Lem, 8 type substitution in a purely abstract environment, p.53

.. G. Lem, 9 equality kinding in an uncontributing environment, p.53

.. G. Lem, 10 equivalence of small types in an uncontributing environment, p.54

.. G. Lem, 11 type decomposition, p.54

.. G. Lem, 12 decomposition of type equivalence, p.56

.. G. Lem, 13 structural dependence of values on their types, p.56

.. G. Lem, 14 triviality of type equivalence in a trivial environment, p.57

.. G. Th, 15 type preservation for expression reduction, p.57

.. G. Lem, 16 type preservation for network structural congruence, p.59

.. G. Cor, 17 type preservation for network reduction, p.59

.. G. Th, 18 type preservation for machine reduction, p.60

.. H. Def, 1 waiting for communication, p.60

H. Lem, 4 reduction in context, p.61

.. H. Th, 9 determinism of machine reduction, p.63

H. Lem, 10 values do not reduce, p.64

.. H. Th, 11 determinism of expression reduction, p.64

.. H. Dis, 65 Def. I.1 revelation of the implementation of a hash, p.65

.. I. Def, 2 partial type substitution associated to an environment, p.65

.. I. Lem, 3 a purely abstract suffix does not change the substitution, p.66

.. I. Lem, 4 stability of types through revelation, p.66

.. I. Lem, 5 distinction of fresh type variables, p.66

.. I. Lem, 6 open interpretation of type equivalence 67 Th. I.7 semantic interpretation of type world judgements, p.69

.. I. Lem, 10 simplicity of the reconstructed type, p.71

.. I. Lem, 11 assurance of correctness of the reconstructed type, p.71

.. I. Lem, 12 validity of the reconstructed type, p.72

.. I. Cor, 13 deciding expression typing through type reconstruction 72 Th. I.14 decidability of type checking, p.72

.. I. Def, 15 user source program, p.73

.. I. Dis, 16 decidability of type checking for user programs, p.73

.. I. Def, 17 bracket elimination subsystem, p.73

.. I. Lem, 18 determinism of bracket elimination, p.73

.. I. Lem, 19 termination of bracket elimination, p.73

.. I. Def, 22 bracketless expressions, p.74

.. I. Def, 23 bracketless reductions, p.74

.. I. Lem, 24 progress and determinism of bracketless expression reduction 74 Th. I.25 bracket erasure preserves expression reduction outcomes, p.74

.. I. Th, 26 bracket erasure preserves reduction outcomes, p.74

.. I. Th, 27 bracket erasure does not add expression reduction outcomes, p.75

.. I. Th, 28 bracket erasure does not add reduction outcomes, p.75

.. J. Def, 1 multiple-let context, p.76

.. J. Lem, 3 correct multiple-let contexts yield ok environments, p.76

.. J. Lem, 4 machine judgement characterisation of correct multiple-let contexts, p.76

.. J. Lem, 5 peeling outer let from a multiple-let context preserves correctness, Def. J, vol.6, p.77

.. J. Def, 7 no shadowing in a multiple-let context, p.77

.. J. Def, 8 environment corresponding to a multiple-let context, p.77

.. J. Def, 9 substitution corresponding to a multiple-let context, p.77

.. J. Lem, 10 substituting through the partial type substitution associated to an environment, p.77

.. J. Lem, 11 partial type substitution associated to an environment via left folding, p.77

.. J. Lem, 13 ok environments are partially, p.77

. J. Lem, 14 partial type substitution associated to an environment, alternative characterisation, p.78

.. J. Lem, 15 correspondence between open and hashed interpretation of type equivalence 78 Th. J.16 coincidence between undyn-time and static type checking, p.80

.. J. Def, 17 list of external names in a multiple-let context, p.81

.. J. Def, 18 external name shadowing, p.81

.. J. Lem, 19 non-shadowing through external names, p.81

.. J. Lem, 20 generalised machine judgement characterisation of correct multiple-let contexts, p.81

. J. Cor, 21 coincidence between undyn-time and static type checking with non-repeated external names . . . . 81 INRIA References Dynamic typing in a statically typed language, ACM TOPLAS, vol.13, issue.2, pp.237-268, 1991.

M. Abadi, L. Cardelli, B. Pierce, and D. Rémy, Abstract, Journal of Functional Programming, vol.5, issue.01, pp.111-130, 1995.
DOI : 10.1145/44501.45065

M. Gavin-bierman, P. Hicks, G. Sewell, K. Stoyle, and . Wansbrough, Dynamic rebinding for marshalling and update, with destruct-time ? Full version available as UCAM-CL-TR-568, Proc. ICFP 2003, 2003.

A. Birrell, G. Nelson, S. Owicki, and E. Wobber, Network objects, Software: Practice and Experience, vol.33, issue.S4, pp.87-130, 1995.
DOI : 10.1002/spe.4380251305

[. Cardelli and X. Leroy, Abstract types and the dot notation, 1990.
URL : https://hal.archives-ouvertes.fr/hal-01499980

D. Dreyer, K. Crary, and R. Harper, A type system for higher-order modules, Proc. 30th POPL, pp.236-249, 2003.
DOI : 10.1145/604131.604151
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.2728

D. Duggan, Type-Safe linking with recursive DLLs and shared libraries, ACM Transactions on Programming Languages and Systems, vol.24, issue.6, pp.711-804, 2002.
DOI : 10.1145/586088.586093
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.3959

J. Furuse and P. Weis, Entrées/sorties de valeurs en Caml, J. Francophones des Langages Applicatifs, 2000.

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

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, 1994.
DOI : 10.1145/174675.176927

R. Harper and G. Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '95, pp.130-141, 1995.
DOI : 10.1145/199448.199475

M. Hicks, S. Weirich, and K. Crary, Safe and Flexible Dynamic Linking of Native Code, Proc. 3rd Workshop on Types in Compilation, pp.147-176, 2000.
DOI : 10.1007/3-540-45332-6_6

]. F. Kna95 and . Knabe, Language Support for Mobile Agents, 1995.

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

J. J. Leifer, G. Peskine, P. Sewell, and K. Wansbrough, Global abstraction-safe marshalling with hash types Available from http, Proc. 8th ICFP, 2003.

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

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

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

[. Pierce and E. Sumii, Relating cryptography and polymorphism, 2000.

]. M. Rob96 and . Robshaw, On recent results for MD2, MD4 and MD5. RSA Laboratories' Bulletin, 1996.

A. Rossberg, Dynamic opacity for abstract types Programming Systems Lab, 2002.

P. Sewell, Modules, abstract types, and distributed versioning, Proc. 28th POPL, pp.236-247, 2001.

A. Christopher, R. Stone, and . Harper, Deciding type equivalence in a language with singleton kinds, Proc. 27th POPL, pp.214-227, 2000.

P. Sewell, P. T. Wojciechowski, and B. C. Pierce, Location-Independent Communication for Mobile Agents: A Two-Level Architecture, Internet Programming Languages CONCUR'96, pp.1-31, 1996.
DOI : 10.1007/3-540-47959-7_1

S. Weirich, Type-safe cast: Functional pearl, Proc. ICFP, pp.58-67, 2000.

S. Weirich, Higher-Order Intensional Type Analysis, Proc. 11th ESOP, 2002.
DOI : 10.1007/3-540-45927-8_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.7120

S. Zdancewic, D. Grossman, and G. Morrisett, Principals in programming languages: A syntactic proof technique main body: $Revision: 1.211 $ $Date: 2003/06/25 09:42:27 $ appendices: $Revision: 1.236 $ $Date, Proc. ICFP rue du Jardin Botanique -BP 101 -54602 Villers-lès-Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rhône-Alpes : 655, avenue de l'Europe -38330 Montbonnot-St, pp.197-207, 1999.