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

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

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

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 ,

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 ,

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

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 ,

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

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 ,

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 ,

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 ,

Type or T hm S ok: no extra condition ,

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

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

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

Since there is no extra condition, we just have to prove that the judgement is derivable ,

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

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

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

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 ,

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 ,

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

7 prefixes of ok environments, p.35 ,

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

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

11 type world judgement, p.37 ,

12 hashes in something, p.37 ,

13 partial order on colours, p.37 ,

15 alternate, informal definition of, p.37 ,

18 stability of values by substitution, p.38 ,

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

20 connection between fv, p.39 ,

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

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

23 expression substitution in environment, p.39 ,

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

2 colour stripping judgements, p.39 ,

4 merging environments, p.41 ,

6 kinds are smaller than Type, p.41 ,

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

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

10 colour change preserves type okedness, p.42 ,

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

12 computing unresolved free variables, p.42 ,

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

14 type preservation by substitution, p.43 ,

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

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

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

19 reflexivity of kind equivalence, p.45 ,

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

21 things have to be ok, p.45 ,

22 weakening kind in the environment, p.47 ,

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

24 type equivalence is a congruence, p.47 ,

25 type substitution in equivalence, p.48 ,

26 reversing subsignaturing judgement, p.48 ,

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

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

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

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

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

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

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

1 shortening typing proof, p.52 ,

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

3 transitivity of kind equivalence, p.52 ,

4 discreteness of subkinding below Type, p.53 ,

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

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

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

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

11 type decomposition, p.54 ,

12 decomposition of type equivalence, p.56 ,

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

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

15 type preservation for expression reduction, p.57 ,

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

17 type preservation for network reduction, p.59 ,

18 type preservation for machine reduction, p.60 ,

1 waiting for communication, p.60 ,

4 reduction in context, p.61 ,

9 determinism of machine reduction, p.63 ,

10 values do not reduce, p.64 ,

11 determinism of expression reduction, p.64 ,

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

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

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

4 stability of types through revelation, p.66 ,

5 distinction of fresh type variables, p.66 ,

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

10 simplicity of the reconstructed type, p.71 ,

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

12 validity of the reconstructed type, p.72 ,

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

15 user source program, p.73 ,

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

17 bracket elimination subsystem, p.73 ,

18 determinism of bracket elimination, p.73 ,

19 termination of bracket elimination, p.73 ,

22 bracketless expressions, p.74 ,

23 bracketless reductions, p.74 ,

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

26 bracket erasure preserves reduction outcomes, p.74 ,

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

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

1 multiple-let context, p.76 ,

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

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

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

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

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

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

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

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

13 ok environments are partially, p.77 ,

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

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

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

18 external name shadowing, p.81 ,

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

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

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

Abstract, Journal of Functional Programming, vol.5, issue.01, pp.111-130, 1995. ,

DOI : 10.1145/44501.45065

Dynamic rebinding for marshalling and update, with destruct-time ? Full version available as UCAM-CL-TR-568, Proc. ICFP 2003, 2003. ,

Network objects, Software: Practice and Experience, vol.33, issue.S4, pp.87-130, 1995. ,

DOI : 10.1002/spe.4380251305

Abstract types and the dot notation, 1990. ,

URL : https://hal.archives-ouvertes.fr/hal-01499980

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

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

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

Syntactic type abstraction, ACM Transactions on Programming Languages and Systems, vol.22, issue.6, pp.1037-1080, 2000. ,

DOI : 10.1145/371880.371887

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

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

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

Language Support for Mobile Agents, 1995. ,

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

Global abstraction-safe marshalling with hash types Available from http, Proc. 8th ICFP, 2003. ,

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

Abstract types have existential type, ACM TOPLAS, vol.10, issue.3, pp.470-502, 1988. ,

The Definition of Standard ML, 1990. ,

Relating cryptography and polymorphism, 2000. ,

On recent results for MD2, MD4 and MD5. RSA Laboratories' Bulletin, 1996. ,

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

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

Deciding type equivalence in a language with singleton kinds, Proc. 27th POPL, pp.214-227, 2000. ,

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

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

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

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