# C EXTENSIONS

In this section we present two extensions of our source language of Section 2, that add let-expressions and records. The former is a minimum requirement for any practical programming language, the latter plays a key role if we want our theory to be applicable to dynamic languages.

## C.1 Let Bindings

### C.1.1 Declarative Type System.
Let bindings can easily be added to the syntax of our language:

$$ \textbf{Expressions} \quad e ::= \dots | \text{let } x = e \text{ in } e \qquad (38) $$

For the reduction semantics, we just add the following notion of reduction and definition of evaluation context:

$$ \text{let } x = v \text{ in } e \quad \rightarrow \quad e\{v/x\} $$

### Evaluation Context
$$ E ::= \dots | \text{let } x = E \text{ in } e $$

and the typing rule is straightforward:

$$ [\text{LET}] \quad \frac{\Gamma \vdash e_1 : t_1 \qquad \Gamma, (x : t_1) \vdash e_2 : t_2}{\Gamma \vdash \text{let } x = e_1 \text{ in } e_2 : t_2} $$

### C.1.2 Intermediate System.
We add the same production as in (38) in the grammar for intermediate expressions. The definition of unwinding is then straightforward:

$$ [\text{let } x = e_1 \text{ in } e_2] = \text{let } x = [e_1] \text{ in } [e_2] $$

The definition of canonical forms instead changes in a more surprising way since we add as atom for let expressions the following canonical form:

$$ \textbf{Atomic expr} \quad a ::= \dots | \text{let } x \text{ in } x \qquad (39) $$

Surprising as it may be, the intuition is rather simple: to produce the atom for the expression `let x = e_1 in e_2` we must replace each subexpression by a variable which would yield something of the form `let x = x_1 in x_2`. It easy to see that since the body of the let-expression is a variable, then the variable `x` is completely useless. The same expressivity can be obtained by specifying only the other two variables, which yields `let x_1 in x_2` and which explains the definition of the atom for let expressions. To say it into a different way, we proceed as before, and define canonical forms so that every subexpression that is not a variable is isolated in the definition of a bind (in this way every such subexpression can be designated by a variable). If we were to proceed as before then we should add to atoms the let expression in which all subexpressions are variables. We then add to the transformation function the following clause to transform the let expressions:

$$ [[\text{let } x = e_1 \text{ in } e_2]] = (\Delta_1; \Delta_2; x_o \mapsto \text{let } x_1 \text{ in } x_2, x_o) \\ \text{where } (\Delta_1, x_1) = [[e_1]], (\Delta_2, x_2) = [[e_2\{x_1/x\}]] $$

yielding the following canonical form for the example expression `let x = \lambda y.y in (x, x)`:

$$ \begin{align*} \text{bind } x_1 &= \lambda y.y \text{ in} \\ \text{bind } x_2 &= (x_1, x_1) \text{ in} \\ \text{bind } x_o &= (\text{let } x_1 \text{ in } x_2) \text{ in } x_o \end{align*} $$

The variable `x` is no longer present in the expression. It is unneeded as it is an alias for the variable `x_1`.
We do the same for algorithmic expressions, since we do not want to add an annotation in an atom $let x_1 in x_2$: such annotations will be directly put on the bind-expressions that bind $x_1$ and $x_2$.

**C.1.3 Annotation Reconstruction Rules.** The extension of the algorithm for reconstruction is straightforward. We add to the clauses of Appendix B.1 the following clause:

$$ [\Gamma \vdash \Box (\text{let } x_1 \text{ in } x_2 \rightsquigarrow t)] \supset \{\Gamma[x_1 \stackrel{\triangle}{=} 1][x_2 \stackrel{\triangle}{=} t]\} \quad (40) $$

In a word, the type $t$ of the expression matches the type of $x_2$, while we also ensure that $x_1$ is well-typed simply by refining its current type by the top type $1$.

$$ [\text{LET}] \quad \Gamma \vdash_R \text{let } x_1 \text{ in } x_2 : t \Rightarrow (\text{let } x_1 \text{ in } x_2, \Gamma[x_1 \stackrel{\triangle}{=} 1][x_2 \stackrel{\triangle}{=} t]) $$

The [LET] rule that defines the algorithm pass for the new atom we added matches the refinement rule: $x_1$ must be well-typed, while the type of $x_2$ refines to the type of the entire expression.

## C.2 Records

In languages such as JavaScript, the fundamental object type is implemented as an extensible record. Record expressions are sometimes an afterthought in the definition of a calculus, as their semantics can typically be reduced to that of the pair. Extending their operations beyond projection to include field update and deletion, however, warrants additional attention.

**C.2.1 Terms.** New expressions are added to the source language to create and manipulate records: the empty record, a record update expression, a field deletion expression, and a field projection expression. Record values consist of empty records and record update expressions whose constituent expressions are themselves values.

$$ \begin{array}{lclcl} \textbf{Expressions} & e & ::= & \dots & | & \{\} | \{e \text{ with } \ell = e\} | e\backslash\ell | e.\ell \\ \textbf{Values} & v & ::= & \dots & | & \{\} | \{v \text{ with } \ell = v\} \end{array} \quad (41) $$

To reduce verbosity, we use syntactic sugar for nonempty records. Assuming all the labels are distinct, $\{\{\{\}\} \text{ with } \ell_1 = e_1\} \text{ with } \ell_2 = e_2\} \dots \text{ with } \ell_n = e_n\}$ is represented by $\{\ell_1 = e_1, \ell_2 = e_2, \dots, \ell_n = e_n\}$.

The record expressions of the source language correspond directly<fnref n="12" /> to operations on objects in JavaScript:

<table><thead><tr><th>JavaScript</th><th>Source Language</th></tr></thead><tbody><tr><td><code>obj.field</code></td><td><code>obj.field</code></td></tr><tr><td><code>delete obj.field</code></td><td><code>obj\field</code></td></tr><tr><td><code>obj.field = val</code></td><td><code>{obj with field = val}</code></td></tr></tbody></table>

**C.2.2 Declarative Type System.** Reduction of record expressions is straightforward. It is worth noting that in this representation, multiple identical labels may exist in a record expression, but this is equivalent to limiting to one label, as projection reduces to the last-applied field, and deletion

<footnote n="12">¹²One important difference is that the operations in JavaScript are effectful. Field update and deletion modify the object on which they are operating, rather than returning a new object. To complicate things further, update and projection operations may actually call setter and getter methods on the object, rather than directly modifying the object's properties. Lastly, property accesses may be forwarded to an object's prototype if not present on the object itself. We use a more naïve model for comparison.</footnote>
removes all instances of a label from the record:

$$ \{v' \text{ with } l = v\} \cdot l \rightsquigarrow v \qquad (42) $$

$$ \{v' \text{ with } l' = v\} \cdot l \rightsquigarrow v' \cdot l \qquad l' \neq l \qquad (43) $$

$$ \{\} \setminus l \rightsquigarrow \{\} \qquad (44) $$

$$ \{v' \text{ with } l = v\} \setminus l \rightsquigarrow v' \setminus l \qquad (45) $$

$$ \{v' \text{ with } l' = v\} \setminus l \rightsquigarrow \{v' \setminus l \text{ with } l' = v\} \qquad l' \neq l \qquad (46) $$

Evaluation of the expressions is performed left-to-right, as in the rest of the language:

$$ \textbf{Evaluation Context} \ E ::= \dots \mid \{E \text{ with } l = e\} \mid \{v \text{ with } l = E\} \mid E \setminus l \mid E \cdot l \qquad (47) $$

### C.2.3 Types.

$$ \textbf{Types} \ t ::= \dots \mid \{f \cdots f\} \mid \{f \cdots f \cdots\} \qquad (48) $$

$$ \textbf{Fields} \ f ::= l = t \mid l = ? t $$

In the syntax for record types, we distinguish between two kinds of record types. An open record type, denoted by `{... ..}`, is the type of records whose labels *include* those explicitly written. A closed record type, denoted by `{...}`, is the type of records whose labels are *exactly* those explicitly written. Formally, this is syntactic sugar for the record types of Frisch [2004], where record types are *quasi constant functions*, that is, functions that map label into types and are constant apart from on a finite number of labels. A closed record type `{l₁ = t₁, l₂ = t₂}` maps `l₁` into `t₁`, `l₂` into `t₂` and *all other labels* into the constant *Undef* meaning that the field is “absent”. *Undef* is a type that is not inhabited by any value of the language. *Undef* and can be seen as the type of the result of projection of a missing label. *Undef* is particular in that it is not considered a normal type, that is, *Undef ∧ 1 = ∅*. This property allows us to encode open record types, by considering them as quasi constant functions where all the labels not explicitly written are mapped to *Undef ∨ 1* (i.e., they are either absent, or they have some type).

The syntax of types does not allow us to explicitly refer to the *Undef* constant. The open/closed record syntax provides a way to set it for the infinitely many constant fields that are not explicitly written in the record type. For a single label, the access to the *Undef* constant is provided via the syntax of fields. There are two kinds of fields. The former, denoted by `l = t`, indicates the field is present in the record. The latter, denoted by `l = ? t` is syntactic sugar for `l = (t ∨ Undef)`, indicating that a label `l` may be present, and if so, it has the type `t`. Note the special case `l = ? ∅`, which indicates that the field for `l` is absent.

$$ t \cdot l = \begin{cases} \min\{u \mid t \le \{l = u \cdots\}\} & \text{if } t \le \{l = 1 \cdots\} \\ \text{Undef} & \text{otherwise} \end{cases} \qquad (49) $$

$$ t_1 + t_2 = \min \left\{ u \mid \begin{array}{l} \forall l \in \text{Labels.} \quad \begin{cases} u \cdot l \ge t_2 \cdot l \\ u \cdot l \ge t_1 \cdot l \lor (t_2 \cdot l \setminus \text{Undef}) \end{cases} & \text{if } t_2 \cdot l \le \neg \text{Undef} \\ \text{Undef} & \text{otherwise} \end{array} \right\} \qquad (50) $$

$$ t \setminus l = \min \left\{ u \mid \begin{array}{l} \forall l' \in \text{Labels.} \quad \begin{cases} u \cdot l' \ge \text{Undef} & \text{if } l' = l \\ u \cdot l' \ge t \cdot l' & \text{otherwise} \end{cases} \\ \text{Undef} & \text{if } l' = l \end{array} \right\} \qquad (51) $$

Three operators are introduced for record types. Record projection (49) represents the union of the possible types the label `l` could have, or is undefined if the record type does not surely have a label `l`. Record concatenation (50) is the right-favored merging of two records. If a label is present in just one of the records, then the type of that label is used. If it is present in both records, the type of the right label is used. Record label deletion (51) marks the label as *Undef*.
The typing rules for records to add to the declarative system are straightforward:

$$
\begin{array}{l @{\quad} l @{\quad} l @{\quad} c @{\quad} c @{\quad} c @{\quad} c @{\quad} c}
\text{[RECORD]} & \overline{\Gamma \vdash \{\} : \{\}} & \text{[UPDATE]} & \frac{\Gamma \vdash e_1 : t_1 \qquad t_1 \le \{\dots\} \qquad \Gamma \vdash e_2 : t_2}{\Gamma \vdash \{e_1 \text{ with } \ell = e_2\} : t_1 + \{\ell = t_2\}} & \text{[DELETE]} & \frac{\Gamma \vdash e : t \qquad t \le \{\dots\}}{\Gamma \vdash e \setminus \ell : t \setminus \ell} & \text{[SELECT]} & \frac{\Gamma \vdash e : t \qquad t \le \{\ell = 1 \dots\}}{\Gamma \vdash e \cdot \ell : t \cdot \ell}
\end{array}
$$

The empty record value has the closed record type. Record update uses the type operator for extension and is defined provided that the type of $e_1$ is a record type (i.e., $t_1 \le \{\dots\}$). Field deletion uses the corresponding type operator and so does field projection provided that the selected field $\ell$ is present the expression $e$ (i.e., $t \le \{\ell = 1 \dots\}$).

### C.2.4 Intermediate Type System.
The record typing rules for the intermediate type system are identical to those in the declarative system. The unwinding rules are described below.

$$
\begin{align*}
\lceil \{\} \rceil &= \{\} \\
\lceil \{e_1 \text{ with } \ell = e_2\} \rceil &= \lceil \{e_1\} \text{ with } \ell = \lceil e_2 \rceil \rceil \\
\lceil e \setminus \ell \rceil &= \lceil e \rceil \setminus \ell \\
\lceil e \cdot \ell \rceil &= \lceil e \rceil \cdot \ell
\end{align*}
$$

### C.2.5 Canonical Forms.
The atomic expressions are, as before, those containing only variables as their subexpressions.

$$ \textbf{Atomic expressions} \quad a ::= \dots | \{\} | \{x \text{ with } \ell = x\} | x.\ell | x \setminus \ell \quad (52) $$

They are obtained by adding to the definition of the transformation function given in Appendix A.7 the following clauses:

$$
\begin{align*}
\llbracket e \setminus \ell \rrbracket &= ((\Delta; x_0 \mapsto x \setminus \ell), x_0) & \text{where } (\Delta, x) &= \llbracket e \rrbracket \\
\llbracket e \cdot \ell \rrbracket &= ((\Delta; x_0 \mapsto x \cdot \ell), x_0) & \text{where } (\Delta, x) &= \llbracket e \rrbracket \\
\llbracket \{e_1 \text{ with } \ell = e_2\} \rrbracket &= ((\Delta_1; \Delta_2; x_0 \mapsto \{x_1 \text{ with } \ell = x_2\}), x_0) & \text{where } (\Delta_1, x_1) &= \llbracket e_1 \rrbracket, (\Delta_2, x_2) &= \llbracket e_2 \rrbracket
\end{align*}
$$

### C.2.6 Annotation Reconstruction Rules.
We add to the clauses of Appendix B.1 the following clauses:

$$
\begin{align}
[\Gamma \vdash \Box (\{\} \rightsquigarrow t)] &\supset \{\} \qquad \{\} \wedge t \approx \emptyset \tag{53} \\
[\Gamma \vdash \Box (\{\} \rightsquigarrow t)] &\supset \{\Gamma\} \qquad \{\} \wedge t \neq \emptyset \tag{54} \\
[\Gamma \vdash \Box (x.\ell \rightsquigarrow t)] &\supset \{\Gamma[x : \overset{\triangle}{=} \{\ell = t \dots\}]\} \tag{55} \\
[\Gamma \vdash \Box (x_1 \text{ with } \ell = x_2 \rightsquigarrow \bigvee_{i \in I} t_i)] &\supset \{\Gamma[x : \overset{\triangle}{=} t_i \setminus \ell + \{\ell =? 1\}] | i \in I, \text{Undef } \leq t_i.\ell\} \tag{56} \\
[\Gamma \vdash \Box (x_1 \text{ with } \ell = x_2 \rightsquigarrow \bigvee_{i \in I} t_i)] &\supset \{\Gamma[x_1 : \overset{\triangle}{=} t_i \setminus \ell + \{\ell =? 1\}] [x_2 : \overset{\triangle}{=} (t_i \wedge \{\ell = 1 \dots\}).\ell] | i \in I\} \tag{57}
\end{align}
$$

The necessary typing refinements for the empty record value are equivalent to those for other constants. For projection, the type of the record is refined only to records containing the projected label with the expected type. Field deletion and update split a union type into its components and share the expression $t_i \setminus \ell + \{\ell =? 1\}$. This expression removes all information about the label $\ell$.
from the record type $t_i$. Note that this cannot be achieved by simply removing the label as in $t_i \setminus \ell$, as this instead sets the record field to $\{\dots \ell =? \emptyset \dots\}$. Indeed, the latter type expression denotes records for which it is statically known that label $\ell$ does not occur. The field deletion rule uses does it for $t_i$ only if the field $\ell$ of $t_i$ is optional or for which there is no information: every $t_i$ for which the field $\ell$ has a given type (i.e., for which $\text{Undef} \not\leq t_i \cdot \ell$) is discarded because it is not possible that $x \setminus \ell$ reduces to a value that has such a type $t_i$. Field update removes any information about $\ell$ in $x_1$ (thus weakening the constraints on it), consider only those $t_i$ which contain records with a field $\ell$ (i.e., for which $t_i \land \{\ell = \mathbf{1} \dots\}$ is not empty), and refines the type of $x_2$ with the type of that field.

Algorithm $\vdash_R$ (Section B.3) is extended with the rule below, plus two rules for the empty record value that we omit since they are the same as the two rules for constants given in Section B.3 (just, replace $\{\}$ for $c$ and $\{\}$ for $b_c$):

$$[SELECTEmpty] \frac{\Gamma(x) \approx \emptyset}{\Gamma \vdash_R x.\ell : t \Rightarrow (x.\ell, \{\Gamma\})}$$

$$[SELECT] \frac{\Gamma(x) \wedge \{\ell = t \dots\} \stackrel{\text{DNF}}{\cong} \bigvee_{i \in I} t_i}{\Gamma \vdash_R x.\ell : t \Rightarrow (x.\ell, \{\Gamma[x : \stackrel{\wedge}{=} t_i]\}_{i \in I})}$$

$$[UPDATEEmpty] \frac{\Gamma(x_1) \times \Gamma(x_2) \approx \emptyset}{\Gamma \vdash_R \{x_1 \text{ with } \ell = x_2\} : t \Rightarrow (\{x_1 \text{ with } \ell = x_2\}, \{\Gamma\})}$$

$$[UPDATE] \frac{\{x_1, x_2\} \subseteq \text{dom}(\Gamma) \quad t \wedge \{\ell = \Gamma(x_2) \dots\} \stackrel{\text{DNF}}{\cong} \bigvee_{i \in I} t_i}{\Gamma \vdash_R \{x_1 \text{ with } \ell = x_2\} : t \Rightarrow (\{x_1 \text{ with } \ell = x_2\}, \{\Gamma[x : \stackrel{\wedge}{=} (t_i \setminus \ell) + \{\ell =? \mathbf{1}\}][x_2 : \stackrel{\wedge}{=} t_i.\ell]\}_{i \in I})}$$

$$[DELETEEmpty] \frac{\Gamma(x) \approx \emptyset}{\Gamma \vdash_R x \setminus \ell : t \Rightarrow (x \setminus \ell, \{\Gamma\})}$$

$$[DELETE] \frac{t \wedge \{\ell =? \emptyset \dots\} \stackrel{\text{DNF}}{\cong} \bigvee_{i \in I} t_i}{\Gamma \vdash_R x \setminus \ell : t \Rightarrow (x \setminus \ell, \{\Gamma[x : \stackrel{\wedge}{=} (t_i \setminus \ell) + \{\ell =? \mathbf{1}\}][x_i : \stackrel{\wedge}{=} t_i.\ell]\}_{i \in I})}$$

These rules work in a way similar to the rules for products (pairs and projections). Each new atom is handled by two cases. In the case where the variable(s) at play have the empty type, the input environment $\Gamma$ is returned as a singleton, denoting success. Otherwise, the relevant record part of the input type is isolated using an intersection with the top record type (augmented with the relevant field), split into a union of records, and the input environment is refined accordingly. In particular, [SELECT] refines the type of $x$ so that it becomes a record type in which the field $\ell$ has a subtype of $t$. The rule [UPDATE] refines the type of $x_1$ to conform the expected type $t$ but without touching any type information about the type of $\ell$ in $x$ (since this information has no effect on the final type of the update) and refines the type of $x_2$ so that it is a subtype of the type of the field $\ell$ in the checked type $t$. Finally, [DELETE] refines the type of $x$ so that it becomes a subtype of the checked type $t$ but without considering and touching the type information of the field $\ell$ in the type of $x$ (since it does not influence the typing of $x \setminus \ell$ whose $\ell$ field is of type $\text{Undef} \lor \emptyset$).
# D PROOFS

## D.1 Declarative Type System

**D.1.1 Parallel Semantics.** One technical difficulty in the proof of the subject reduction property is that reducing an expression *e* might break the use of a [⊤] rule. Indeed, if in the original typing derivation a rule [⊤] substitutes multiple occurrences of the expression *e* by a variable *x*, reducing one occurrence of *e* but not the others would alter the application of this rule (correlation between the reduced *e* and the other occurrences of *e* will be lost).

To circumvent this issue, we introduce a notion of parallel reduction which forces to reduce all occurrences of a sub-expression at the same time.

The idea is to remember, when applying a reduction under a context, which reduction has been performed inside this context. For that, each step of reduction is labeled with a statement of the form $e_1 \mapsto e_2$ which denotes the inner reduction that has been performed. Then, this label is used by the context rule (rule [κ] below) which will substitute occurrences of $e_1$ by $e_2$ everywhere in the expression (not only under the current context).

The semantics based on parallel reduction is given below.

For convenience, we denote $e \stackrel{e \mapsto e'}{\rightsquigarrow} e'$ by $e \stackrel{\text{Id}}{\rightsquigarrow} e'$ and by $e \stackrel{\text{Not}}{\rightsquigarrow} e'$ a step of reduction of the parallel semantics, regardless of the value on the top of the arrow.

$$ (\lambda x.e)v \stackrel{\text{Id}}{\rightsquigarrow} e\{v/x\} \qquad (58) $$

$$ \pi_1(v_1, v_2) \stackrel{\text{Id}}{\rightsquigarrow} v_1 \qquad (59) $$

$$ \pi_2(v_1, v_2) \stackrel{\text{Id}}{\rightsquigarrow} v_2 \qquad (60) $$

$$ (v \in \tau) \ ? \ e_1 : e_2 \stackrel{\text{Id}}{\rightsquigarrow} e_1 \qquad \text{if } v \in \tau \qquad (61) $$

$$ (v \in \tau) \ ? \ e_1 : e_2 \stackrel{\text{Id}}{\rightsquigarrow} e_2 \qquad \text{if } v \in \neg \tau \qquad (62) $$

The contexts are not exactly those of the original semantics: nesting of contexts is now handled by the rule [κ]. This yields the following definition:

$$ \textbf{Evaluation Context} \quad \bar{E} ::= v[\quad] | \quad e | (v, \quad) | (\quad, e) | (\quad, \tau) ? e : e $$

**Context reductions:**

$$ [\kappa] \frac{e \stackrel{e_r \mapsto e'_r}{\rightsquigarrow} e'}{\bar{E}[e] \stackrel{e_r \mapsto e'_r}{\rightsquigarrow} (\bar{E}[e']) \{e'_r/e_r\}} $$

Here is an example of a reduction step using the parallel semantics:

$$ [\kappa] \frac{[\beta] \quad \underset{(\lambda x. x + 1) 1 \stackrel{(\lambda x. x+1)}{\rightsquigarrow} 2}{\text{\hspace{2em}}} \quad \underset{(\lambda x. x + 1) 1 \stackrel{(\lambda x. x+1)}{\rightsquigarrow} 2}{\text{\hspace{2em}}} \quad 2}{\text{\hspace{2em}}} \text{if } (\lambda x. x + 1) 1 \in \text{Int} \text{ then } (\lambda x. x + 1) 1 \text{ else } 0} \quad \underset{(\lambda x. x+1) 1 \stackrel{1 \mapsto 2}{\rightsquigarrow}}{\text{\hspace{2em}}} \text{if } 2 \in \text{Int} \text{ then } 2 \text{ else } 0} $$

Notice that the rule [κ] applies a substitution from an expression to an expression. This is formally defined as follows:
**DEFINITION D.1 (EXPRESSION SUBSTITUTIONS).** Expression substitutions, ranged over by $\rho$, map an expression into another expression. The application of an expressions substitution $\rho$ to an expression $e$, noted $e\rho$ is the capture avoiding replacement defined as follows:

* If $e' \equiv_{\alpha} e''$, then $e''\{e/e'\} = e$.

* If $e' \not\equiv_{\alpha} e''$, then $e''\{e/e'\}$ is inductively defined as

$$c\{e/e'\} = c$$

$$x\{e/e'\} = x$$

$$(e_1 e_2)\{e/e'\} = (e_1\{e/e'\})(e_2\{e/e'\})$$

$$(\lambda x.e_0)\{e/e'\} = \lambda x.e_0 \qquad x \in fv(e')$$

$$(\lambda x.e_0)\{e/e'\} = \lambda x.(e_0\{e/e'\}) \qquad x \notin fv(e) \cup fv(e')$$

$$(\lambda x.e_0)\{e/e'\} = \lambda y.((e_0\{y/x\})\{e/e'\}) \qquad x \notin fv(e), x \in fv(e'), y \text{ fresh}$$

$$(\pi_i e_0)\{e/e'\} = \pi_i(e_0\{e/e'\})$$

$$(e_1, e_2)\{e/e'\} = (e_1\{e/e'\}, e_2\{e/e'\})$$

$$((e_1 \in t) ? e_2 : e_3)\{e/e'\} = (e_1\{e/e'\} \in t) ? e_2\{e/e'\} : e_3\{e/e'\}$$

Notice that the expression substitutions are up to alpha-renaming and perform only one pass.

**D.1.2 Normalization Lemmas.** See 3 for the full delcarative system.

In the proofs below, the $[\vee+]$ and $[\wedge+]$ rules will be used instead of the $[\vee]$ and $[\wedge]$ rules.

**LEMMA D.2 (MONOTONICITY).** If $\Gamma \vdash e : t$ and $\Gamma' \le \Gamma$, then $\Gamma' \vdash e : t$.

**PROOF.** By induction on the derivation of the judgement $\Gamma \vdash e : t$. $\square$

**LEMMA D.3 (INTERSECTION).** If $\Gamma \vdash e : t_1$ and $\Gamma \vdash e : t_2$, then $\Gamma \vdash e : t_1 \wedge t_2$.

**PROOF.** Straightforward, by using a rule $[\wedge+]$. $\square$

**LEMMA D.4 (UNION).** If $\Gamma, x : t_1 \vdash e : t$ and $\Gamma, x : t_2 \vdash e : t$, then $\Gamma, x : (t_1 \vee t_2) \vdash e : t$.

**PROOF.** Straightforward, by using a rule $[\vee+]$ of the following form:

$$[\vee+] \frac{\Gamma, x : (t_1 \vee t_2) \vdash x : t_1 \vee t_2 \qquad \Gamma, x : (t_1 \vee t_2), y : t_1 \vdash e : t \qquad \Gamma, x : (t_1 \vee t_2), y : t_2 \vdash e : t}{\Gamma, x : (t_1 \vee t_2) \vdash e\{x/y\} : t}$$

$\square$

**LEMMA D.5 (NORMALIZATION OF $[\le]$ RULES).** Any derivation of $\Gamma \vdash e : t$ can be transformed so that every application of $[\le]$ is:

* At the root of the derivation, or

* The first premise of a $[\epsilon_1]$ or $[\epsilon_2]$ rule, or

* The nth premise ($n \ge 2$) of a $[\vee+]$ rule, or

* The premise of a $[\times E_1]$ or $[\times E_2]$ rule, or

* The first premise of a $[\to E]$ rule

**PROOF.** We can transform any derivation into a derivation that satisfies these properties. We proceed by induction on the depth of the derivation, without counting the $[\le]$ rules nor the axioms $([Ax]$ and $[CONST])$.

When there are two consecutive $[\le]$ rules, they can trivially be merged into one $[\le]$ rule.

The base case is trivial (if there is a $[\le]$ rule, it is at the root of the derivation).
Now we consider the last rule of the derivation which is not a `[≤]`, and assume that its premises satisfy these properties.

If the last rule is a `[∧+]` with one of its premises being a `[≤]` rule:

$$ [\leq] \frac{\frac{A}{\Gamma \vdash e : t_1'} \qquad \frac{B_i}{\Gamma \vdash e : t_i} \quad \forall i \in I}}{\Gamma \vdash e : t_1 \wedge \bigwedge_{i \in I} t_i} \rightarrow [\leq] \frac{\frac{A}{\Gamma \vdash e : t_1'} \qquad \frac{B_i}{\Gamma \vdash e : t_i} \quad \forall i \in I}}{\Gamma \vdash e : t_1' \wedge \bigwedge_{i \in I} t_i} $$

If the last rule is a `[∀+]` with its first premise being a `[≤]`, we apply the following transformation and then proceed inductively on the transformed $B_i$ premises:

$$ [\forall+] \frac{\frac{A}{\Gamma \vdash e' : s'} \qquad \frac{B_i}{\Gamma, : s_i \vdash e : t} \quad \forall i \in I}}{\Gamma \vdash e' / x : t} $$

↓

$$ [\forall+] \frac{\frac{A}{\Gamma \vdash e' : \bigvee_{i \in I} (s_i \wedge s')} \qquad \frac{\text{Easily derived from } B_i}{\Gamma, (x : s_i \wedge s') \vdash e : t} \quad \forall i \in I}}{\Gamma \vdash e' / x : t} $$

The other cases are trivial or similar. □

**LEMMA D.6 (NORMALIZATION OF `[∧+]` RULES).** Any derivation of $\Gamma \vdash e : t$ can be transformed so that all the applications of `[∧+]` have only `[→I]` rules as premises.

**PROOF.** We can transform any derivation into a derivation that satisfies these properties. First, we apply the `[≤]` normalization lemma on the derivation, so that `[∧+]` rules cannot have a `[≤]` rule as premise. Then, we proceed by induction on the size of the derivation (i.e. the total number of rule applications) without counting the applications of `[≤]` nor the axioms ([Ax] and [CONST]).

The base case (size 0) is trivially true, as there are no instances of `[∧+]`.

In the inductive case, if the last rule of the derivation is not a `[∧+]`, we can directly conclude by induction. If the last rule is a `[∧+]` with one of its premises being another `[∧+]` rule, we can easily merge the two `[∧+]` rules and proceed inductively on the result.

If the last rule is a `[∧+]` with one of its premises being a `[∀+]` rule, we can apply the following transformation and proceed inductively on the premises:
$$ [\begin{array}{c} \text{[}\vee\text{]} \\ \text{[}^+\text{]} \end{array}] \frac{\frac{A}{\Gamma \vdash e' : \bigvee_{i \in I} s_i} \qquad \frac{B_i}{\Gamma, x : s_i \vdash e : t_1} \qquad \forall i \in I} {\Gamma \vdash e\{e'/x\} : t_1} \qquad \frac{D_j}{\Gamma \vdash e\{e'/x\} : t_j} \qquad \forall j \in J $$

↓

$$ \frac{A}{\Gamma \vdash e' : \bigvee_{i \in I} s_i} \qquad \frac{\substack{\text{Easily derived from } B_i \\ \text{[}^+\text{]}}} {\Gamma, x : s_i \vdash \bar{e} : t_1} \qquad \frac{\substack{\text{Easily derived from } D_j \\ \text{[}^+\text{]}}} {\Gamma, x : s_i \vdash \bar{e} : t_j} \qquad \forall j \in J $$

$$ \text{with } \bar{e} = e\{x/e'\} $$

If the last rule is a `[^+]` and all its premises are a `[→E]` rule, we can apply the following transformation and proceed inductively on the premises:

$$ [\begin{array}{c} \text{[}→\text{E}] \\ \text{[}^+\text{]} \end{array}] \frac{\frac{A_i}{\Gamma \vdash e_1 : t_1^i \rightarrow t_2^i} \qquad \frac{B_i}{\Gamma \vdash e_2 : t_1^i} \qquad \forall i \in I} {\Gamma \vdash e_1 e_2 : t_2^i} $$

↓

$$ [\begin{array}{c} \text{[}≤\text{]} \\ \text{[}→\text{E}] \end{array}] \frac{\frac{A_i}{\Gamma \vdash e_1 : t_1^i \rightarrow t_2^i} \qquad \forall i \in I} {\Gamma \vdash e_1 e_2 : (\bigwedge_{i \in I} t_1^i) \rightarrow (\bigwedge_{i \in I} t_2^i)} \qquad \frac{B_i}{\Gamma \vdash e_2 : t_1^i} \qquad \forall i \in I} {\Gamma \vdash e_2 : \bigwedge_{i \in I} t_1^i} $$

The other cases are trivial. □

LEMMA D.7 (NORMALIZATION OF `[V+]` RULES). Any derivation of $\Gamma \vdash e : t$ can be transformed so that every application of `[V+]` that uses the substitution $\{e'/x\}$ satisfies one of these conditions:

* It is the nth premise ($n \ge 2$) of a (possibly empty) succession of `[V+]` rules at the root of the derivation

* It is the nth premise ($n \ge 2$) of a (possibly empty) succession of `[V+]` rules used as a premise of a `[→I]` rule that introduces a variable y such that $y \in fv(e')$

* It is the nth premise ($n \ge 2$) of a (possibly empty) succession of `[V+]` rules used as a premise of a `[V+]` rule that introduces a variable y such that $y \in fv(e')$
PROOF. We can transform any derivation into a derivation that satisfies these properties. First, we apply the [∧+] normalization lemma on the derivation, so that [∧+] rules cannot have a [∨+] rule as premise. Then, we proceed by structural induction on the derivation.

The base cases are trivially true, as there is no instance of [∨+].

Now, we consider the last rule of the derivation and assume that its premises satisfy these properties.

If the last rule is a [∨+] with another [√+] rule as first premise:

$$ \frac{[\vee+] \quad \frac{\Gamma \vdash e'' : \bigvee_{j \in J} s_j}{\Gamma \vdash e' \{e''/y\} : \bigvee_{i \in I} t_i} \quad \forall j \in J}{\Gamma \vdash e \{e'/y\} : t} \quad \forall i \in I $$

$$ \frac{\begin{array}{c} A \\ \Gamma \vdash e'' : \bigvee_{j \in J} s_j \end{array}}{[\vee+] \quad \frac{B_j}{\Gamma, y : s_j \vdash e' : \bigvee_{i \in I} t_i} \quad \text{Easily derived from } C_i \quad \forall i \in I} \quad \forall j \in J $$ $$ \frac{\Gamma, y : s_j \vdash e \{e'/x\} : t}{\Gamma \vdash (e \{e'/x\}) \{e''/y\} : t} $$ $$ \text{with } y \notin \text{fv}(e) \text{ (y can be renamed otherwise)} $$

If the last rule is a [→I], introducing a variable y, with a [√+] rule as premise, such that y ∉ fv(e'):

$$ \frac{[\vee+] \quad \frac{A}{\Gamma, y : t_1 \vdash e' : \bigvee_{i \in I} s_i} \quad \frac{B_i}{\Gamma, y : t_1, x : s_i \vdash e : t_2} \quad \forall i \in I}{[\to I] \quad \frac{\Gamma, y : t_1 \vdash e \{e'/x\} : t_2}{\Gamma \vdash \lambda y. (e \{e'/x\}) : t_1 \to t_2} $$

$$ \frac{\text{Easily derived from } A}{[\vee+] \quad \frac{\Gamma \vdash e' : \bigvee_{i \in I} s_i}{\Gamma \vdash (\lambda y. e) \{e'/x\} : t_1 \to t_2} \quad \forall i \in I} \quad \forall i \in I $$

In order to apply the transformation above, we can swap two independent [√+] rules if necessary: if we have a [√+] rule that uses the substitution {e''/y} as the nth premise (n ≥ 2) of another [√+] rule that uses the substitution {e'/x}, and such that x ∉ fv(e''), then we can swap the order of these two [√+] rules in the following way.
$$
\begin{array}{r@{\quad}l@{\qquad}l}
\frac{A}{\Gamma \vdash e' : t_1 \lor \bigvee_{i \in I} t_i} & [\lor +] & \frac{B}{\Gamma, x : t_1 \vdash e'' : \bigvee_{j \in J} s_j} \quad \frac{C_j}{\Gamma, x : t_1, y : s_j \vdash e : t} \quad \forall j \in J \\
& & \frac{D_i}{\Gamma, x : t_i \vdash e\{e''/y\} : t} \quad \forall i \in I \\
& [\lor +] & \frac{}{} \Gamma \vdash (e\{e''/y\})\{e'/x\} : t \\
& & \downarrow \\
& & \frac{}{} \text{Easily derived from } B \\
& & \frac{\Gamma \vdash e'' : \bigvee_{j \in J} s_j}{\Gamma \vdash e'' : \bigvee_{i \in I} t_i} \\
& & \frac{}{} \text{Easily derived from } A \\
& [\lor +] & \frac{C_j}{\Gamma, y : s_j \vdash e' : t_1 \lor \bigvee_{i \in I} t_i} \quad \frac{D_i}{\Gamma, y : s_j, x : t_1 \vdash \bar{e} : t} \quad \forall i \in I \\
& & \frac{}{} \frac{\Gamma, y : s_j, x : t_1 \vdash \bar{e} : t}{\Gamma, y : s_j \vdash e\{e'/x\} : t} \quad \forall j \in J \\
& [\lor +] & \frac{}{} \Gamma \vdash (\bar{e}\{e'/x\})\{e''/y\} : t \\
& & \text{with } \bar{e} = e\{y/e''\}
\end{array}
$$

If the last rule is a [≤] with a [∨+] rule as premise:

$$
\begin{array}{r@{\quad}l@{\qquad}l}
& \frac{A}{\Gamma \vdash e' : \bigvee_{i \in I} s_i} & \frac{B_i}{\Gamma, x : s_i \vdash e : t'} \quad \forall i \in I \\
[\le] & \frac{}{} \frac{\Gamma \vdash e\{e'/x\} : t'}{\Gamma \vdash e\{e'/x\} : t} & \\
& \downarrow & \\
& \frac{A}{\Gamma \vdash e' : \bigvee_{i \in I} s_i} & \frac{B_i}{\Gamma, x : s_i \vdash e : t'} \quad \forall i \in I \\
[\lor +] & \frac{}{} \frac{\Gamma \vdash e\{e'/x\} : t}{\Gamma \vdash e\{e'/x\} : t} &
\end{array}
$$

If the last rule is a [→E] with a [∨+] rule as first premise:
$$ [\begin{array}{c} A \\ \Gamma \vdash e' : \bigvee_{i \in I} s_i \\ \hline [\to E] \end{array}] \quad \frac{\frac{\frac{A}{\Gamma \vdash e' : \bigvee_{i \in I} s_i} \qquad \frac{B_i}{\Gamma, x : s_i \vdash e_1 : t_1 \to t_2} \qquad \forall i \in I}}{\Gamma \vdash e_1\{e'/x\} : t_1 \to t_2} \quad \frac{C}{\Gamma \vdash e_2 : t_1} \quad \frac{\Gamma \vdash (e_1\{e'/x\})e_2 : t_2}{\Gamma \vdash (e_1 e_2)\{e'/x\} : t_2} $$

↓

$$ [\begin{array}{c} A \\ \Gamma \vdash e' : \bigvee_{i \in I} s_i \\ \hline [\to E] \end{array}] \quad \frac{\frac{B_i}{\Gamma, x : s_i \vdash e_1 : t_1 \to t_2} \qquad \text{Easily derived from C} \qquad \frac{\Gamma, x : s_i \vdash e_2 : t_1}{\Gamma, x : s_i \vdash e_1 e_2 : t_2} \qquad \forall i \in I}{\Gamma \vdash (e_1 e_2)\{e'/x\} : t_2} $$

with $x \notin \text{fv}(e_2)$ ($x$ can be renamed otherwise)

If the last rule is a $[\to E]$ with a $[\vee+]$ rule as second premise, the transformation is similar. The other cases are trivial or similar. □

**LEMMA D.8 (DELETION OF VALUE SUBSTITUTIONS).** *Any derivation of $\Gamma \vdash e : t$ can be transformed so that it does not contain any $[\vee+]$ rule with $e'$ being a value.*

**PROOF.** First, we apply the $[\le]$, $[\wedge]$ and $[\vee+]$ normalization lemmas and above to the derivation. In particular, this ensures that there are no $[\vee+]$ rules in the derivations of the first premises of the $[\vee+]$ rules, except as premise of a $[\to I]$ rule.

Now, let's suppose one of the $[\vee+]$ rule of our derivation is using a substitution $\{e'/x\}$ with $e'$ being a value. Its first premise is of the form $\Gamma \vdash v : t'$ with $v \equiv e'$ and $t' \cong \bigvee_{i \in I} t_i$. As the $[\le]$ and $[\vee+]$ rules have been normalized, the derivation of this premise does not contain any $[\vee+]$ rule nor $[\le]$ rule, except inside the derivation of the premise of a $[\to I]$ rule.

It can easily be deduced that $t'$ can be constructed with the following syntax:

$$ \textbf{Value Type} \quad \bar{t} ::= b \mid t \to t \mid \bar{t} \times \bar{t} \mid \bar{t} \wedge \bar{t} $$

A type constructed with the syntax above cannot be decomposed into a non-trivial union (in particular, a conjunction of arrows cannot be decomposed into a non-trivial union of arrows). Thus, we can deduce that the decomposition $t' \cong \bigvee_{i \in I} t_i$ is such that $\exists i \in I. \forall j \in I. t_i \le t_j$.

Then, it becomes easy to remove the application of the $[\vee+]$ rule from our derivation by replacing it by one of its premises (the one of the form $\Gamma, x : t_i \vdash e : t$ for some $\Gamma, e$ and $t$) in which the applications of the rule $[Ax]$ applied to $v$ have been replaced by the first premise.

This transformation can be used successively to remove all such $[\vee+]$ rules in the derivation. □

Note that all the normalization lemmas above are compatible: by applying the transformations successively, we can transform a derivation into another one that satisfies all the lemmas D.5, D.6, D.7 and D.8.

### D.1.3 Subject-Reduction.

**PROPERTY D.9.** If $\Gamma \vdash v : \tau$, then $v \in \tau$.

**PROOF.** Straightforward, by induction on the derivation of the judgement $\Gamma \vdash v : \tau$. Note that the case of lambda-abstractions is trivial as $\tau$ can only be $\emptyset \to \{\emptyset\}$.
**LEMMA D.10 (SUBSTITUTION LEMMA).** If $\Gamma$, ($x : t_o$) $\vdash$ $e : t$ and $\Gamma \vdash e' : t_o$, then $\Gamma \vdash e\{e'/x\} : t$.

**PROOF.** Straightforward, by using the rule $[\nV]$ with $t_1 = t_2 = t_o$. $\square$

The proof of the subject reduction requires a more permissive notion of reduction. In particular, for the inductive case $[\nV+]$, we need our induction hypothesis to be able to reduce under any context and to consider that variables are values.

Thus, we introduce the following notion of reduction. Note that it does not contain any context rule (reductions can only happen at top-level): the context is handled in the statement of the subject reduction.

$$ \textbf{Extended Values} \quad \bar{v} ::= c \mid \lambda x.e \mid (\bar{v}, \bar{v}) \mid x \qquad (63) $$

$$ (\lambda x.e)\bar{v} \rightsquigarrow_{\Gamma} e\{\bar{v}/x\} \qquad (64) $$

$$ \pi_1(\bar{v}_1, \bar{v}_2) \rightsquigarrow_{\Gamma} \bar{v}_1 \qquad (65) $$

$$ \pi_2(\bar{v}_1, \bar{v}_2) \rightsquigarrow_{\Gamma} \bar{v}_2 \qquad (66) $$

$$ (v \in \tau) \ ? e_1 : e_2 \rightsquigarrow_{\Gamma} e_1 \qquad \text{if } v \in \tau \qquad (67) $$

$$ (v \in \tau) \ ? e_1 : e_2 \rightsquigarrow_{\Gamma} e_2 \qquad \text{if } v \in \neg \tau \qquad (68) $$

**THEOREM D.11 (GENERALIZED SUBJECT REDUCTION).** If $\Gamma \vdash e : t$ and $e_o \rightsquigarrow_{\Gamma} e'_o$, then $\Gamma \vdash e\{e'_o/e_o\} : t$.

**PROOF.** We apply all the normalization lemmas above to the derivation of the judgement $\Gamma \vdash e : t$, and we proceed by structural induction on it. We denote by $\rho$ the substitution $\{e'_o/e_o\}$ and by $e'$ the expression $e\rho$. If $e$ contains no occurrence of $e_o$ (modulo alpha-renaming), this theorem is trivial. Thus, we will suppose in the following that $e$ contains at least one occurrence of $e_o$.

Depending on the last rule used:

**[CONST]** Impossible case ($e$ cannot contain a reducible expression).

**[Ax]** Impossible case ($e$ cannot contain a reducible expression).

**[≤]** By induction on the premise $\Gamma \vdash e : t'$ (with $t' \le t$), we get a derivation for $\Gamma \vdash e' : t'$, thus we can derive $\Gamma \vdash e' : t$ by using $[\le]$.

**[∧]** Trivial (by induction on the premises as in the previous case).

**[→I]** We have $e' \equiv \lambda x. (e_1\rho)$, thus we can conclude by induction on the premise $\Gamma, x : t_1 \vdash e_1 : t_2$ as in the previous case.

**[×I]** We have $e' \equiv (e_1\rho, e_2\rho)$, thus we can conclude by induction on the premises as in the previous case.

**[→E]** We have $e \equiv e_1 e_2$. If $e_o$ is a subexpression of $e_1$ and/or $e_2$, we conclude trivially by induction (as in the previous cases).

Otherwise, the reduction $e_o \rightsquigarrow_{\Gamma} e'_o$ uses the rule 58 and we know that $e_o \equiv e \equiv (\lambda x. e_\lambda)\bar{v}_2$ and $e'_o \equiv e' \equiv e_\lambda\{\bar{v}_2/x\}$.

We have the following premises:

$$ (1) \Gamma \vdash \lambda x. e_\lambda : t_1 \rightarrow t_2 \text{ (with } t_2 \cong t) $$

$$ (2) \Gamma \vdash \bar{v}_2 : t_1 $$

As the $[\nV+]$ rules of our derivation satisfy the normalization lemma D.7, we can extract from the first premise a collection of derivations of the judgements $\Gamma, x : s_i \vdash e_\lambda : s'_i$ for $i \in I$, such that $\bigwedge_{i \in I} s_i \rightarrow s'_i \le t_1 \rightarrow t_2$.

Let's consider a partition $\{u_j\}_{j \in J}$ of $t_1$ that satisfies the following property:

$$ \forall i \in I. \forall j \in J. u_j \le s_i \text{ or } u_j \wedge s_i = \emptyset. $$
We can suppose that $J$ is not empty: the case $t_1 \approx \emptyset$ is trivial. For every $j \in J$, we pose $I_j = \{i \in I \mid s_i \wedge u_j \neq \emptyset\} (I_j$ cannot be empty as $t_1 \leq \bigvee_{i \in I} s_i)$. Note that for all $j \in J$ and $i \in I_j$, we have $u_j \leq s_i$.

According to the monotonicity lemma (D.2), for every $j \in J$ and $i \in I_j$ we can derive the judgement $\Gamma, x : u_j \vdash e_\lambda : s'_i$. Moreover, as $\wedge_{i \in I} s_i \rightarrow s'_i \leq t_1 \rightarrow t_2$, we have for every $j \in J$: $\wedge_{i \in I_j} s'_i \leq t_2$.

Consequently, for every $j \in J$, we can derive the judgement $\Gamma, x : u_j \vdash e_\lambda : t_2$ using the intersection lemma (D.3) on the judgements $\{\Gamma, x : u_j \vdash e_\lambda : s'_i\}_{i \in I_j}$. Using the union lemma (D.4) on the judgements $\{\Gamma, x : u_j \vdash e_\lambda : t_2\}_{i \in I_j}$, we can derive $\Gamma, x : t_1 \vdash e_\lambda : t_2$.

As $\Gamma \vdash \bar{v}_2 : t_1$, we can deduce, using the substitution lemma (D.10), a derivation for $\Gamma \vdash e_\lambda(\bar{v}_2/x) : t_2$.

[×E₁] We have $e \equiv \pi_1 e_1$. If $e_\circ$ is a subexpression of $e_1$, we conclude trivially by induction.

Otherwise, the reduction $e_\circ \rightsquigarrow_{\mathrm{Ex}} e'_\circ$ uses the rule 59 and we know that $e_\circ \equiv e \equiv \pi_1(\bar{v}_1, \bar{v}_2)$ and $e'_\circ \equiv e' \equiv \bar{v}_1$.

As the [v+] rules of our derivation satisfy the normalization lemma D.7, we can extract from the premise $\Gamma \vdash (\bar{v}_1, \bar{v}_2) : t_1 \times t_2$ a collection of derivations of the judgements $\Gamma \vdash \bar{v}_1 : s_i$ and $\Gamma \vdash \bar{v}_2 : s'_i$ for $i \in I$, such that $\wedge_{i \in I} (s_i \times s'_i) \leq t_1 \times t_2$. This last property implies $\wedge_{i \in I} s_i \leq t_1$. Therefore, we can conclude this case by using the intersection lemma (D.3) on the judgements $\{\Gamma \vdash \bar{v}_1 : s_i\}_{i \in I}$.

[×E₂] Similar to the previous case.

[v+] We have $e \equiv e_1\{e_2/x\}$ (conclusion of the [v+] rule), and thus $e' \equiv (e_1\{e_2/x\})\{e'_\circ/e_\circ\}$. We know that $e_\circ$ does not contain $x$ as a free variable (otherwise there would be no occurrence of $e_\circ$ in $e_1\{e_2/x\}$). Moreover, $e'_\circ$ does not contain $x$ neither, because a reduction step cannot introduce a new free variable.

There are several cases:

* $e_\circ$ does not contain $e_2$ and $e_2$ does not contain $e_\circ$. In this case, we have:

$e' \equiv (e_1\{e_2/x\})\{e'_\circ/e_\circ\} \equiv (e_1\{e'_\circ/e_\circ\})\{e_2/x\}$. Thus, we can easily conclude with a [v+] rule by keeping the first premise and applying the induction hypothesis on the others.

* $e_2$ contains $e_\circ$. In this case, we pose $e'_2 = e_2\{e'_\circ/e_\circ\}$.

We have $e' \equiv (e_1\{e_2/x\})\{e'_\circ/e_\circ\} \equiv (e_1\{e'_\circ/e_\circ\})\{e'_2/x\}$. We can easily derive $\Gamma \vdash e'_2 : \bigvee_{i \in I} t_i$ by induction on the first premise, and $\Gamma, x : t_i \vdash e_1\{e'_\circ/e_\circ\} : t$ for all $i \in I$ by induction on the others. Thus, we can derive $\Gamma \vdash (e_1\{e'_\circ/e_\circ\})\{e'_2/x\} : t$ using the [v+] rule.

* $e_\circ$ contains $e_2$ as a strict subexpression. In this case, we pose $e_\circ^1 = e_\circ\{x/e_2\}$ and $e_\circ^2 = e'_\circ\{x/e_2\}$.

We have $e' \equiv (e_1\{e_2/x\})\{e'_\circ/e_\circ\} \equiv (e_1\{e_2^2/e_\circ^1\})\{e_2/x\}$. Again, there are several cases:

$e_\circ^1 \rightsquigarrow_{\mathrm{Ex}} e_\circ^2$ This is the case if $e_2$ only appears in $e_\circ$ inside of a lambda abstraction, in a branch of a typecase, or in a value used as argument of an application or projection. In this case, we can easily conclude with a [v+] rule by keeping the first premise and applying the induction hypothesis on the others.

$e_\circ^1 \equiv x\bar{v}$ (for any $\bar{v}$) It means that $e_2$ is a lambda-abstraction. We can skip this case without loss of generality according to the lemma D.8.

$e_\circ^1 \equiv \pi_1 x$ It means that $e_2$ is a value. We can skip this case without loss of generality according to the lemma D.8.

$e_\circ^1 \equiv \pi_2 x$ Similar to the previous case.

$e_\circ^1 \equiv (x \in \tau) ? e_t : e_e$ (for any $\tau, e_t, e_e$) Similar to the previous case.

[0] We have $e \equiv (e_1 \in \tau) ? e_2 : e_3$. As values cannot have the type $\emptyset$, we know that $e_1$ is not a value. Thus, $e' \equiv (e_1 \rho \in \tau) ? e_2 \rho : e_3 \rho$. We can derive $\Gamma \vdash e_1 \rho : \emptyset$ by induction on the premise, thus we can derive $\Gamma \vdash e' : \emptyset$ by using [0].
[ε₁] We have e ≡ (e₁ ∈ τ) ? e₂ : e₃. There are three cases:

e' ≡ (e₁ρ ∈ τ) ? e₂ρ : e₃ρ We can easily conclude by induction on the premises.

e' ≡ e₂ We can easily conclude by induction on the second premise.

e' ≡ e₃ This case is impossible. Indeed, it implies that e₁ is a value. As Γ ⊢ e₁ : τ (first premise), we can deduce using the property D.9 that e₁ ∈ τ, which contradicts e ~ Ex e₃.

[ε₂] Similar to the previous case.

☐

COROLLARY D.12 (SUBJECT REDUCTION). If Γ ⊢ e : t and e ~ e', then Γ ⊢ e' : t.

PROOF. The derivation of the reduction e ~ e' may use several [κ] rules, but it must end with a reduction e₀ ~ e'₀ that does not use rule [κ]. As the ~ Ex semantics and the parallel semantics only differ on the context rule, we also have e₀ ~ Ex e'₀.

Moreover, we have e' ≡ e{e'₀/e₀}. Thus, we can conclude by using the previous theorem.

☐

D.1.4 Progress.

THEOREM D.13 (GENERALIZED PROGRESS). If Γ ⊢ e : t and if there is no evaluation context E and variable x such that e ≡ E[x], then either e is a value or ∃e'. e ~ e'.

PROOF. We apply all the normalization lemmas above to the derivation of the judgement Γ ⊢ e : t, and we proceed by structural induction on it.

Depending on the last rule used:

[CONST] Trivial (e is a value).

[Ax] Impossible case (e cannot be a variable).

[≤] Trivial (by induction on the premise).

[∧+] Trivial (by induction on one of the premises).

[→I] Trivial (e is a value).

[×I] We have e ≡ (e₁, e₂).

* If e₁ is not a value, we know by applying the induction hypothesis that e₁ can be reduced. Thus, e can also be reduced using the rule [κ].

* If e₁ is a value, then we can apply the induction hypothesis on the second premise (as e₁ is a value, we know that ∀E, x. e₂ ≠ E[x]). It gives that either e₂ is a value or it can be reduced. We can easily conclude in both cases (if e₂ is a value, then e is also a value, otherwise, e can be reduced using the rule [κ]).

[→E] We have e ≡ e₁e₂, with Γ ⊢ e₁ : s → t and Γ ⊢ e₂ : s.

* If e₁ is not a value, we know by applying the induction hypothesis that e₁ can be reduced. Thus, e can also be reduced using the rule [κ].

* If e₁ is a value, we can apply the property D.9 on it. As Γ ⊢ e₁ : Ø → 1, it gives that e₁ ∈ Ø → 1 and thus e₁ ≡ λx. e₀. Moreover, we can apply the induction hypothesis on the second premise (as e₁ is a value, we know that ∀E, x. e₂ ≠ E[x]). It gives that either e₂ is a value or it can be reduced. We can easily conclude in both cases (if e₂ is a value, then e can be reduced using the rule 58, otherwise, e can be reduced using the rule [κ]).

[×E₁] We have e ≡ π₁e₀, with Γ ⊢ e₀ : t × s. By induction on the premise, we know that e₀ is either a value or it can be reduced. If e₀ can be reduced, then e can also be reduced using the rule [κ]. Otherwise, as Γ ⊢ e₀ : 1 × 1, we know by using the property D.9 that e₀ ∈ 1 × 1. Thus, e₀ ≡ (v₁, v₂) (with v₁ and v₂ two values) and consequently e can be reduced using the rule 59.

[×E₂] Similar to the previous case.

[∀+] We have e ≡ e₀{e'/x}, with Γ ⊢ e' : ∨i∈I tᵢ and ∀i ∈ I. Γ, x : tᵢ ⊢ e₀ : t. There are two cases:
* There exists a reduction context $E$ such that $e_o \equiv E[x]$. In this case, we know that there is no reduction context $E'$ and variable $y$ such that $e' \equiv E'[y]$, otherwise we would have $e \equiv E[E'[y]]$. Thus, we can apply the induction hypothesis on the first premise. It gives that either $e'$ is a value or it can be reduced. The case where $e'$ is a value can be skipped without loss of generality according to the lemma D.8. Thus, we can assume that $e'$ can be reduced. Consequently, $e$ can also be reduced using the rule [κ].

* There is no reduction context $E$ such that $e_o \equiv E[x]$. We also know that there is no reduction context $E$ and variable $y$ such that $y \neq x$ and $e_o \equiv E[y]$, otherwise we would have $e \equiv E[y]$. Thus, we can apply the induction hypothesis on the second premise. It gives that either $e_o$ is a value or it can be reduced. We can easily conclude in both cases (if $e_o$ is a value, then $e$ is also a value, and if $e_o$ can be reduced, then $e$ can also be reduced).

[0] We have $e \equiv (e_o \in \tau) ? e_1 : e_2$, with $\Gamma \vdash e_o : \emptyset$. As values cannot have the type $\emptyset$, we know that $e_o$ is not a value. Thus, by induction on the premise, we know that $e_o$ can be reduced. Consequently, $e$ can be reduced using the rule [κ].

[1] We have $e \equiv (e_o \in \tau) ? e_1 : e_2$, with $\Gamma \vdash e_o : \tau$. By induction on this premise, we know that $e_o$ is either a value or it can be reduced. If $e_o$ is a value, then $e$ can be reduced using the rule 61. Otherwise, $e_o$ can be reduced and thus $e$ can also be reduced using the rule [κ].

[2] Similar to the previous case.

COROLLARY D.14 (PROGRESS). If $\emptyset \vdash e : t$, then either $e$ is a value or $\exists e'$. $e \leadsto e'$.

PROOF. We can deduce from $\emptyset \vdash e : t$ that there is no evaluation context $E$ and variable $x$ such that $e \equiv E[x]$. Thus, we can apply the generalized progress theorem above. □

### D.1.5 Equivalence of the Semantics. See 2.3 for the semantics of the paper.

PROPERTY D.15 (INCLUSION OF $\leadsto$ IN $\sim$). For any $e$ and $v$, if $e \leadsto^* v$, then $e \leadsto^* v$. Moreover, for any $e$, if $e \leadsto^* (e \text{ diverges with } \leadsto)$, then $e \leadsto^* (e \text{ diverges with } \sim)$.

PROOF. For any $e_1$ and $e_2$, we will use the notation $e_1 \leadsto_{\text{Top}} e_2$ to denote a reduction $e_1 \leadsto e_2$ that applies at top-level (i.e. under the empty evaluation context). Moreover, we will denote by $C$ an expression with exactly one hole (it is more general than an evaluation context $E$).

First, we can easily prove by induction the following property:

for any context $E$ and expressions $e, e', e''$, if $E[e] \stackrel{e' \to e}{\leadsto} e''$, then $e'' \equiv E\{e'/e\}[e']$ and $e \leadsto_{\text{Top}} e'$ and $E[e] \leadsto E[e']$.

Then, we show that for any context $E$ and expressions $e, e', e''$, $e_1, \dots, e_n$, if $E[e] \stackrel{e' \to e}{\leadsto} e''$ and $\forall i \in [1..n]$. $e_i \leadsto_{\text{Top}} e'_i$, then for any $C$ such that $C\{e'_1/e_1\} \cdots \{e'_n/e_n\} \equiv E$, there exists $C'$ such that $C[e] \leadsto^* C'[e']$ and $C'\{e'_1/e_1\} \cdots \{e'_n/e_n\} \{e'/e\}[e'] \equiv e''$. The idea behind this result is that:

* If $C$ is an evaluation context, we can directly conclude with the property above.

* Otherwise, we can successively reduce in $C[E]$ the expressions $e_i$ such that $\exists E. E[e_i] \equiv C[e]$ using the fact that $\forall i \in [1..n]$. $e_i \leadsto_{\text{Top}} e'_i$, until $C$ becomes an evaluation context.

The lemma we want to prove can easily be deduced from this result. □

Note that the other inclusion is also true, but is not required to prove the safety of our type system.

THEOREM D.16 (TYPE SAFETY). For any expression $e$, if $\emptyset \vdash e : t$, then either $e \leadsto^* v$ with $\emptyset \vdash v : t$ or $e \leadsto^* (e \text{ diverges})$.

PROOF. Straightforward application of D.12, D.14 and D.15. □
## D.2 Intermediate Type System

See 3 for the full declarative system and 4 for the full intermediate system.

### D.2.1 Soundness.

**LEMMA D.17.** If $\Gamma \vdash e : t$ is derivable and $x \notin \Gamma$, then $\forall e' . \Gamma \vdash e\{e'/x\}$ is derivable.

**PROOF.** As $x \notin \Gamma$, the derivation of $\Gamma \vdash e : t$ cannot use the rule [Ax] on $x$, and thus it does not contain any typing derivation for $x$ as a sub-derivation. Thus, we can transform the derivation of $\Gamma \vdash e : t$ into a derivation of $\Gamma \vdash e\{e'/x\}$ by replacing every occurrence of $x$ by $e'$ (straightforward induction). $\square$

**THEOREM D.18 (SOUNDNESS).** If $\Gamma \vdash_I e : t$ then $\Gamma \vdash [e] : t$

**PROOF.** We proceed by structural induction on the typing derivation of $\Gamma \vdash_I e : t$. Depending on the last rule used (we use the variable names defined in this rule):

[CONST-INT] Trivial.

[AX-INT] Trivial.

[→I-INT] By induction on the premises, we get $\forall j \in J. \Gamma, x : t_j \vdash [e] : s_j$. By applying the rule [→I] on each of these derivations, we get $\forall j \in J. \Gamma \vdash \lambda x. [e] : t_j \rightarrow s_j$. We conclude by applying the rule [∧+].

[→E-INT] We have $t \approx t_1 \circ t_2$. According to the definition of $\circ$, we can deduce that $t_1 \le t_2 \rightarrow t$. Moreover, by induction on the premises, we get $\Gamma \vdash [e_1] : t_1$ and $\Gamma \vdash [e_2] : t_2$. By applying the [≤] rule, we can derive $\Gamma \vdash [e_1] : t_2 \rightarrow t$. We can then easily conclude with an application of the rule [→E].

[×I-INT] By induction on the premises, we get $\Gamma \vdash [e_1] : t_1$ and $\Gamma \vdash [e_2] : t_2$. We conclude by applying the rule [×I].

[×E₁-INT] By induction on the premise, we get $\Gamma \vdash [e] : t$. According to the definition of $p_i$, we can deduce that $t \le (\pi_1 t) \times 1$. By applying the [≤] rule, we can derive $\Gamma \vdash [e] : (\pi_1 t) \times 1$. We conclude by applying the rule [×E₁].

[×E₂-INT] Similar to the previous case.

[◊-INT] Similar to the previous case.

[ε₁-INT] By induction on the premises, we get $\Gamma \vdash [e] : t_0$ with $t_0 \le t$ and $\Gamma \vdash [e_1] : t_1$. By applying the [≤] rule, we can derive $\Gamma \vdash [e] : t$. We conclude by applying the rule [ε₁].

[ε₂-INT] Similar to the previous case.

[V₁-INT] By induction on the premise, we get $\Gamma \vdash [e_2] : s$. As $x \notin \Gamma$, we can transform our derivation into a derivation of $\Gamma \vdash [e_2]\{[e_1]/x\} : s$ using lemma D.17.

[V₂-INT] By induction on the premises, we get $\Gamma \vdash [e_1] : \bigvee_{j \in J} t_j$ and $\forall j \in J. \Gamma, x : t_j \vdash [e_2] : s_j$. Using the rule [≤], we can derive $\forall j \in J. \Gamma, x : t_j \vdash [e_2] : \bigvee_{j \in J} s_j$. We conclude by applying the rule [⊕+] (it gives a derivation for $\Gamma \vdash [e_2]\{[e_1]/x\} : \bigvee_{j \in J} s_j$).

### D.2.2 Completeness. See A.8 for all the definitions relative to the canonical form and the MSC-form.

**LEMMA D.19 (MONOTONICITY).** If $\Gamma \vdash_I e : t$ and $\Gamma' \le \Gamma$, then $\Gamma' \vdash_I e : t'$ with $t' \le t$.

More generally, in any derivation for $\Gamma \vdash_I e : t$, we can replace any subderivation $\Gamma_\circ \vdash_I e_\circ : t_\circ$ by a derivation $\Gamma_\circ \vdash_I e_\circ : t'_\circ \le t_\circ$ and still keep a valid derivation for $\Gamma \vdash_I e : t' \le t$ by doing some minor transformations to the rest of the derivation, which involve:

* Refinement of some types in the derivation,

* Refinement of the splits made by a $[\vee_1]$ rule (it may imply the removing of some branches and the strengthening of the environment of some other branches),
• Use of a [0-INT] rule instead of a [ε₁-INT] or [ε₂-INT] rule.

PROOF. Straightforward induction on the typing derivation of Γ ⊢<sub>I</sub> **e** : t.

☐

LEMMA D.20 (INTERSECTION). If Γ ⊢<sub>I</sub> **e** : t₁ and Γ ⊢<sub>I</sub> **e** : t₂, then Γ ⊢<sub>I</sub> **e** : t ≤ t₁ ∧ t₂.

PROOF. It is a straightforward induction on the typing derivations of Γ ⊢<sub>I</sub> **e** : t₁ and Γ ⊢<sub>I</sub> **e** : t₂.
We use the monotonicity lemma (D.19) when needed.

Here is the transformation to apply when both Γ ⊢<sub>I</sub> **e** : t₁ and Γ ⊢<sub>I</sub> **e** : t₂ use [V₂-INT] as last rule.

$$
\frac{\displaystyle\frac{\Gamma \vdash_I \mathbf{a} : \bigvee_{j \in J} t_j}{\Gamma \vdash_I \mathrm{bind} x = \mathbf{a} \mathrm{in} \mathbf{k} : \bigvee_{j \in J} s_j \approx t} \qquad \frac{\displaystyle\frac{\Gamma \vdash_I \mathbf{a} : \bigvee_{j \in J'} t'_j}{\Gamma \vdash_I \mathrm{bind} x = \mathbf{a} \mathrm{in} \mathbf{k} : \bigvee_{j \in J'} s'_j \approx t'}}{\Gamma \vdash_I \mathrm{bind} x = \mathbf{a} \mathrm{in} \mathbf{k} : \bigvee_{j \in J'} s'_j \approx t'} \qquad \downarrow
$$

$$
\frac{\displaystyle\frac{\Gamma \vdash_I \mathbf{a} : t_o \approx \bigvee_{i \in I} u_i}{\Gamma \vdash_I \mathrm{bind} x = \mathbf{a} \mathrm{in} \mathbf{k} : \bigvee_{i \in I} v_i \le t \wedge t'} \qquad \text{Derived by induction on one of the } B_j \text{ and } B'_j}{\Gamma \vdash_I \mathrm{bind} x = \mathbf{a} \mathrm{in} \mathbf{k} : \bigvee_{i \in I} v_i \le t \wedge t'}
$$
$$
\text{Derived by induction on } A \text{ and } A' \qquad \text{with } \{u_i\}_{i \in I} = \text{partition}(\{t_j \wedge t_o\}_{j \in J} \cup \{t'_j \wedge t_o\}_{j \in J'})
$$

The case when both Γ ⊢<sub>I</sub> **e** : t₁ and Γ ⊢<sub>I</sub> **e** : t₂ use [→I-INT] as last rule is quite similar (the new split to use is partition of the union of the two original splits).

The other cases are straightforward.

☐

PROPERTY D.21. *For any intermediate expression e, [term([e])] = [e].*

PROOF. Straightforward structural induction on **e**.

☐

In the following, we extend the function term so that it can take an arbitrary intermediate expression as second argument instead of just a variable.

LEMMA D.22. If Γ, (x : s) ⊢<sub>I</sub> **e** : t and Γ ⊢<sub>I</sub> term(Δ, x) : s, then Γ ⊢<sub>I</sub> term(Δ, **e**) : t' with t' ≤ t.

PROOF. We proceed by induction on the size of Δ.

If Δ = ε, the property is trivial (we can directly use the rule [Ax-INT]).

Otherwise, we have Δ $\stackrel{\text{def}}{=} y \mapsto a$; Δ' and term(Δ, x) = bind y = a in term(Δ', x) . The last rule of the derivation of Γ ⊢<sub>I</sub> term(Δ, x) : s can be:

[V₁-INT] In this case, we have the premise Γ ⊢<sub>I</sub> term(Δ', x) : s and thus, by induction, we can deduce Γ ⊢<sub>I</sub> term(Δ', e) : t' with t' ≤ t. We can derive Γ ⊢<sub>I</sub> term(Δ, e) : t' by using the rule [V₁-INT].

[V₂-INT] In this case, we have the premises Γ ⊢<sub>I</sub> **a** : ∨<sub>j∈J</sub> t<sub>j</sub> and ∀j ∈ J. Γ, y : t<sub>j</sub> ⊢<sub>I</sub> term(Δ', x) : s<sub>j</sub> with s ≈ ∨<sub>j∈I∩J</sub> s<sub>j</sub>. As Γ, (x : s) ⊢<sub>I</sub> **e** : t and ∀j ∈ J. s<sub>j</sub> ≤ s, we know by monotonicity (D.19) that ∀j ∈ J. Γ, (x : s<sub>j</sub>) ⊢<sub>I</sub> **e** : t'<sub>j</sub> with t'<sub>j</sub> ≤ t. By induction, we can deduce ∀j ∈ J. Γ, y : t<sub>j</sub> ⊢<sub>I</sub> term(Δ', e) : t'<sub>j</sub>. We can derive Γ ⊢<sub>I</sub> term(Δ, e) : ∨<sub>j∈J</sub> t'<sub>j</sub> by using the rule [V₂-INT].

☐
**LEMMA D.23.** If $\Gamma$, $(x_1 : s) \vdash_I \text{ term}(\Delta_2, x_2) : t$ and $\Gamma \vdash_I \text{ term}(\Delta_1, x_1) : s$, then $\Gamma \vdash_I \text{ term}((\Delta_1; \Delta_2), x_2) : t'$ with $t' \le t$.

*PROOF.* Straightforward application of the previous lemma with $\boldsymbol{e} = \text{term}(\Delta_2, x_2)$. □

**PROPERTY D.24.** If $\Gamma \vdash_I \boldsymbol{e} : t$ then $\Gamma \vdash_I \text{ term}(\llbracket \boldsymbol{e} \rrbracket) : t'$ with $t' \le t$.

*PROOF.* We proceed by structural induction on the expression $\boldsymbol{e}$.

c Trivial.

x Trivial.

λx. e The last rule of the derivation of $\Gamma \vdash_I e : t$ is [→I-INT]. By induction on its premises, we get $\forall j \in J. \Gamma, x : t_j \vdash_I \text{ term}(\llbracket e \rrbracket) : s'_j$ with $s'_j \le s_j$. We can derive $\Gamma \vdash_I \text{ term}(\llbracket \lambda x. e \rrbracket) : \bigwedge_{j \in J} s'_j$ by applying the rules [→I-INT] and [v₂-INT].

$\pi_1 e$ The last rule of the derivation of $\Gamma \vdash_I e : t$ is [×E-INT]. By induction on its premise, we get $\Gamma \vdash_I \text{ term}(\llbracket e \rrbracket) : t'$ with $t' \le t \le 1 \times 1$ (we use the same variable names as the rule). Let us note $(\Delta, x) \stackrel{\text{def}}{=} \llbracket e \rrbracket$. We can trivially derive $\Gamma, x : t' \vdash_I \text{ term}((x_o \mapsto \pi_i x), x_o) : \pi_1(t')$. Thus, by applying D.23, we can deduce $\Gamma \vdash_I \text{ term}((\Delta; x_o \mapsto \pi_i x), x_o) : \pi_1(t')$.

$\pi_2 e$ Similar to the previous case.

$\boldsymbol{e}_1 \boldsymbol{e}_2$ The last rule of the derivation of $\Gamma \vdash_I e : t$ is [→E-INT]. By induction on its premises, we get $\Gamma \vdash_I \text{ term}(\llbracket e_1 \rrbracket) : t'_1$ with $t'_1 \le t_1 \le \emptyset \to 1$, and $\Gamma \vdash_I \text{ term}(\llbracket e_2 \rrbracket) : t'_2$ with $t'_2 \le t_2 \le \text{dom}(t_1)$ (we use the same variable names as the rule). By monotonicity (D.19) we also have $\Gamma, x_1 : t'_1 \vdash_I \text{ term}(\llbracket e_2 \rrbracket) : t'_2$. Let us note $(\Delta_1, x_1) \stackrel{\text{def}}{=} \llbracket e_1 \rrbracket$ and $(\Delta_2, x_2) \stackrel{\text{def}}{=} \llbracket e_2 \rrbracket$. We can trivially derive $\Gamma, x_1 : t'_1, x_2 : t'_2 \vdash_I \text{ term}((x_o \mapsto x_1 x_2), x_o) : t'_1 \circ t'_2$. Thus, by applying D.23, we can deduce $\Gamma, x_1 : t'_1 \vdash_I \text{ term}((\Delta_2; x_o \mapsto x_1 x_2), x_o) : t'_1 \circ t'_2$. By applying D.23 again, we can finally deduce $\Gamma \vdash_I \text{ term}((\Delta_1; \Delta_2; x_o \mapsto x_1 x_2), x_o) : t'_1 \circ t'_2$.

($e_1, e_2$) Similar to the previous case.

($e_o \in \tau$) ? $e_1 : e_2$ The last rule of the derivation of $\Gamma \vdash_I e : t$ can be $\emptyset$-INT, $[\in_1$-INT] or $[\in_2$-INT]. We will only focus on the $[\in_1$-INT] case here, but the other cases use the same ideas. By induction on the premises of the $[\in_1$-INT] rule, we get $\Gamma \vdash_I \text{ term}(\llbracket e_o \rrbracket) : t'_o \le t_o \le \tau$ and $\Gamma \vdash_I \text{ term}(\llbracket e_1 \rrbracket) : t'_1 \le t_1$ (we use the same variable names as the rule). By monotonicity (D.19) we also have $\Gamma, x_o : t'_o \vdash_I \text{ term}(\llbracket e_1 \rrbracket) : t'_1$. Let us note $(\Delta_o, x_o) \stackrel{\text{def}}{=} \llbracket e_o \rrbracket$, $(\Delta_1, x_1) \stackrel{\text{def}}{=} \llbracket e_1 \rrbracket$ and $(\Delta_2, x_2) \stackrel{\text{def}}{=} \llbracket e_2 \rrbracket$. We can trivially derive $\Gamma, x_o : t'_o, x_1 : t'_1 \vdash_I \text{ term}((\Delta_2; x \mapsto (x_o \in \tau) ? x_1 : x_2), x) : t'_1$ (we use the rule $[\vee_1]$ to skip the definition $\Delta_2$). Thus, by applying D.23, we can deduce $\Gamma, x_o : t'_o \vdash_I \text{ term}((\Delta_1; \Delta_2; x \mapsto (x_o \in \tau) ? x_1 : x_2), x) : t'_1$. By applying D.23 again, we can finally deduce $\Gamma \vdash_I \text{ term}((\Delta_o; \Delta_1; \Delta_2; x \mapsto (x_o \in \tau) ? x_1 : x_2), x) : t'_1$.

**bind** $x = e_1$ **in** $e_2$ If the last rule of the derivation of $\Gamma \vdash_I e : t$ is $[\vee_1$-INT], we can derive $\Gamma \vdash_I \text{ term}(\llbracket e_2 \rrbracket) : s'$ with $s' \le s$ by induction on the premise. We can easily derive $\Gamma \vdash_I \text{ term}(\llbracket e \rrbracket) : s'$ from that by using the $[\vee_1$-INT] rule.

Now we can suppose that the last rule of the derivation of $\Gamma \vdash_I e : t$ is $[\vee_2$-INT]. By induction on its premises, we get $\Gamma \vdash_I \text{ term}(\llbracket e_1 \rrbracket) : t'$ with $t' \le \bigvee_{j \in J} t_j$, as well as $\forall j \in J. \Gamma, x : t_j \vdash_I \text{ term}(\llbracket e_2 \rrbracket) : s'_j$ with $s'_j \le s_j$. Let us note $(\Delta_1, x_1) \stackrel{\text{def}}{=} \llbracket e_1 \rrbracket$ and $(\Delta_2, x_2) \stackrel{\text{def}}{=} \llbracket e_2 \rrbracket$. We can trivially derive $\Gamma, x_1 : t' \vdash_I \text{ term}(x \mapsto x_1, x) : t'$. Moreover, from $\forall j \in J. \Gamma, x : t_j \vdash_I \text{ term}(\llbracket e_2 \rrbracket) : s'_j$, we can derive by monotonicity (D.19) $\forall j \in J. \Gamma, x : t_j \wedge t' \vdash_I \text{ term}(\Delta_2, x_2) : s''_j$ with $s''_j \le s'_j$. Thus, by using the rule $[\vee_2$-INT], we can derive $\Gamma, x_1 : t' \vdash_I ((x \mapsto x_1, \Delta_2), x_2) : \bigvee_{j \in J} s''_j$. By applying D.23, we can deduce $\Gamma \vdash_I ((\Delta_1, x \mapsto x_1, \Delta_2), x_2) : \bigvee_{j \in J} s''_j$.

□

**PROPERTY D.25 (EQUIVALENCE OF MSC-FORMS).** If $\kappa_1$ and $\kappa_2$ are two MSC-forms and $[\kappa_1] \equiv_\alpha [\kappa_2]$, then $\kappa_1 \equiv_\kappa \kappa_2$.
**PROOF.** Let $e \equiv_{\alpha} [\kappa_1] \equiv_{\alpha} [\kappa_2]$. Without loss of generality, we can suppose that every variable in $e$ has a unique name (we can always alpha-rename a variable when there is a conflict). We also suppose that every variable in $\kappa_1$ and $\kappa_2$ (from bindings and abstractions) have a unique name. Let us consider the set $S$ of all the distinct subexpressions of $e$.

To each binding $bind x = a \ in \ \kappa$ in $\kappa_1$ or $\kappa_2$, we associate the expression $E(x)$ obtained by starting from $a$ and recursively inlining the definitions of the variables used (for variables that come from a binding). In other word, we associate to every bound variable the unwinding of its definition.

As $\kappa_1$ and $\kappa_2$ are in MSC-form, we know according to the property 4 of the MSC-form that every binding is used later. Thus, for every binding $bind x = a \ in \ \kappa$, we know that $E(x)$ will appear in $e$ and thus $E(x) \in S$.

From the properties 1 and 2 of the MSC-form definition, we can deduce that for every binding $bind x = a \ in \ \kappa$ in $\kappa_1$ or $\kappa_2$, $E(x)$ is unique (there is no other binding $bind y = a' \ in \ \kappa'$ such that $E(x) = E(y)$). It can be easily proved by induction on the number of bindings in the context of our binding $bind x = a \ in \ \kappa$. From that, we can deduce that there is a one-to-one correspondence between the bindings of $\kappa_1$ and the elements of $S$, and between the bindings of $\kappa_2$ and the elements of $S$.

Thus, $\kappa_1$ and $\kappa_2$ have the exact same bindings modulo alpha-renaming (each binding corresponding to an expression of $S$). Consequently, the only difference between $\kappa_1$ and $\kappa_2$ is the location of these bindings. In particular, each binding is localized by:

* The lambda-abstraction it is in (if any) and

* The relative order of the binding (with respect to the other bindings) in this lambda-abstraction (or at top-level)

The property 3 of the MSC-form definition ensures that every binding is located in the outermost lambda-abstraction possible: a binding can only be nested inside a lambda-abstraction if its definition depends (directly or not) on the variable introduced by this abstraction.

Finally, the only difference between $\kappa_1$ and $\kappa_2$ is the relative order between the independent bindings that are in the same lambda-abstraction (or at top-level). This order can be rearranged with the rewriting rule 22 of the equivalence relation $\equiv_{\kappa}$, thus we have $\kappa_1 \equiv_{\kappa} \kappa_2$. $\square$

**LEMMA D.26.** Let $e_1, e_2, C, \Gamma$ and $t$. If $\Gamma \vdash t_0$. $\Gamma_0 \vdash_I e_1 : t_0 \Rightarrow \Gamma_0 \vdash_I e_2 : t'_0 \le t_0$ and if $\Gamma \vdash_I C[e_1] : t$, then $\Gamma \vdash_I C[e_2] : t' \le t$.

**PROOF.** We can transform the derivation $\Gamma \vdash_I C[e_1] : t$ into a derivation for $\Gamma \vdash_I C[e_2] : t'$:

(1) We replace the relevant occurrence of $e_1$ by $e_2$ at the root of the derivation.

(2) We propagate this change. We stop when we reach a subderivation of the form $\Gamma' \vdash_I e_1 : s$ that should be transformed into $\Gamma' \vdash_I e_2 : s$.

(3) For each such subderivation $\Gamma' \vdash_I e_1 : s$, we replace it by a subderivation for $\Gamma' \vdash_I e_2 : s'$ with $s' \le s$ (we use the hypothesis $\forall \Gamma_0 \forall t_0. \Gamma_0 \vdash_I e_1 : t_0 \Rightarrow \Gamma_0 \vdash_I e_2 : t'_0 \le t_0$).

(4) By monotonicity (D.19), we can propagate the changes on the resulting type and we get a derivation for $\Gamma' \vdash_I C[e_2] : t'$ with $t' \le t$.

<figure><img src="image_6.png" /></figure>

**PROPERTY D.27.** If $\Gamma \vdash_I \kappa : t$ and $\kappa \equiv_{\kappa} \kappa'$, then $\exists t' \le t$ such that $\Gamma \vdash_I \kappa' : t'$.

**PROOF.** First, let's assume the equivalence rule of $\equiv_{\kappa}$ only applies at top-level (i.e. not under an arbitrary context). We have a case for each rule:

22 (→) If the derivation $\Gamma \vdash_I \text{bind } x_1 = a_1 \text{ in bind } x_2 = a_2 \text{ in } \kappa : t$ uses the rule [V₁-INT] for at least one of the two bindings, then the transformation into a derivation for $\Gamma \vdash_I \text{bind } x_2 = a_2 \text{ in bind } x_1 = a_1 \text{ in } \kappa : t'$ is trivial.
Otherwise, we can use the following transformation:

$$
\begin{array}{c}
\displaystyle\frac{A}{\Gamma \vdash_I \mathbf{a}_1 : \bigvee_{j \in J} t_j} \\
\\
\begin{array}{c}
\begin{array}{c}
\frac{B_j}{\Gamma, x_1 : t_j \vdash_I \mathbf{a}_2 : \bigvee_{k \in K_j} t'_{j,k}} \qquad \frac{C_{j,k}}{\Gamma, x_1 : t_j, x_2 : t'_{j,k} \vdash_I \mathbf{k} : s'_{j,k}}
\end{array} \\
\frac{[\vee_2\text{-INT}]}{\Gamma, x_1 : t_j \vdash_I \text{ bind } x_2 = \mathbf{a}_2 \text{ in } \mathbf{k} : \bigvee_{k \in K_j} s'_{j,k} \approx s_j}
\end{array} \\
\\
\frac{[\vee_2\text{-INT}]}{\Gamma \vdash_I \text{ bind } x_1 = \mathbf{a}_1 \text{ in bind } x_2 = \mathbf{a}_2 \text{ in } \mathbf{k} : \bigvee_{j \in J} s_j \approx t} \\
\\
\downarrow \\
\\
\begin{array}{c}
\text{Easily derived from any of the } B_j \\
\\
\frac{\Gamma \vdash_I \mathbf{a}_2 : \bigvee_{i \in I} u_i}{\Gamma \vdash_I \mathbf{a}_2 : \bigvee_{i \in I} u_i}
\end{array} \\
\\
\begin{array}{c}
\text{Easily derived from } A \\
\\
\frac{x_2 : u_i \vdash_I \mathbf{a}_1 : \bigvee_{j \in J} t_j}{\Gamma, x_2 : u_i \vdash_I \mathbf{a}_1 : \bigvee_{j \in J} t_j}
\end{array} \\
\\
\begin{array}{c}
\text{Easily derived by monotonicity from one of the } C_{j,k} \\
\\
\frac{[\vee_2\text{-INT}]}{\Gamma, x_2 : u_i, x_1 : t_j \vdash_I \mathbf{k} : v_{i,j} \leq s_j} \\
\\
\frac{[\vee_2\text{-INT}]}{\Gamma, x_2 : u_i \vdash_I \text{ bind } x_1 = \mathbf{a}_1 \text{ in } \mathbf{k} : \bigvee_{j \in J} v_{i,j} \leq t}
\end{array} \\
\\
\text{with } \{u_i\}_{i \in I} = \text{partition}(\{t'_{j,k} \mid j \in J, k \in K_j\})
\end{array}
$$

22 (←) Similar to the other direction (the rule is symmetric).

The general case (where the equivalence rule can apply under an arbitrary context) can be
deduced by an immediate application of the lemma D.26. □

PROPERTY D.28. If $\mathbf{\kappa} \equiv_{\mathbf{\kappa}'} \mathbf{\kappa}'$, then $[\mathbf{\kappa}] \equiv_{\alpha} [\mathbf{\kappa}']$.

PROOF. First, let's assume the rule 22 applies at top-level on the expression bind $x_1 = \mathbf{a}_1$ in bind $x_2 = \mathbf{a}_2$ in $\mathbf{k}$. As $x_1 \notin \text{fv}(\mathbf{a}_2)$ and $x_2 \notin \text{fv}(\mathbf{a}_1)$, we have $\mathbf{k}\{\mathbf{a}_1/x_1\}\{\mathbf{a}_2/x_2\} = \mathbf{k}\{\mathbf{a}_2/x_2\}\{\mathbf{a}_1/x_1\}$ and thus the unwinding remains unchanged.

The general case can easily be deduced with the observation that $\forall C, \kappa_1, \kappa_2$. $[\kappa_1] \equiv_\alpha [\kappa_2] \Rightarrow [C[\kappa_1]] \equiv_\alpha [C[\kappa_2]]$ □

In the following, we use the notation $\varphi$ to designate either an atom $\mathbf{a}$ or a canonical expression $\mathbf{\kappa}$.

LEMMA D.29. If $\Gamma \vdash_I \varphi : t$ and $\varphi \rightarrow \varphi'$, then $\exists t' \le t$ such that $\Gamma \vdash_I \varphi' : t'$.

PROOF. First, let's assume that the $\rightarrow$ rule applies at top-level (i.e. not under an arbitrary context).
We have a case for each rewriting rule:

23 If the derivation $\Gamma \vdash_I \mathbf{x}_1 = \mathbf{a}_1$ in bind $\mathbf{x}_2 = \mathbf{a}_2$ in $\mathbf{k} : t$ uses the rule $[\vee_1\text{-INT}]$ for at least one of the two bindings, then the transformation into a derivation for $\Gamma \vdash_I \mathbf{x}_1 = \mathbf{a}_1$ in $\mathbf{k}\{\mathbf{x}_1/\mathbf{x}_2\} : t'$ is trivial.
Otherwise, we can use the following transformation:

$$ \frac{\frac{A}{\Gamma \vdash_I a_1 : \bigvee_{j \in J} t_j}}{\frac{B_j}{\Gamma, x_1 : t_j \vdash_I a_2 : \bigvee_{k \in K_j} t'_{j,k}}} \qquad \frac{C_{j,k}}{\Gamma, x_1 : t_j, x_2 : t'_{j,k} \vdash_I \kappa : s'_{j,k}} \\ \frac{\Gamma, x_1 : t_j \vdash_I \text{bind } x_2 = a_2 \text{ in } \kappa : \bigvee_{k \in K_j} s'_{j,k} \approx s_j}{\Gamma \vdash_I \text{bind } x_1 = a_1 \text{ in bind } x_2 = a_2 \text{ in } \kappa : \bigvee_{j \in J} s_j \approx t} $$

↓

$$ \frac{\frac{A}{\Gamma \vdash_I a_1 : \bigvee_{i \in I} u_i}}{\Gamma \vdash_I \text{bind } x_1 = a_1 \text{ in } \kappa : \bigvee_{i \in I} v_i \le t} \qquad \frac{\text{Easily derived by monotonicity from one of the } C_{j,k}}{\Gamma, x_1 : u_i \vdash_I \kappa : \{x_1/x_2\} : v_i \le t} \\ \text{with } \{u_i\}_{i \in I} = \text{partition}(\{t_j\}_{j \in J} \cup \{t'_{j,k} \mid j \in J, k \in K_j\}) $$

24 If the derivation $\Gamma \vdash_I x = a \text{ in } \kappa : t$ uses the rule $[\text{V}_1-\text{INT}]$ for the bind, then the transformation into a derivation for $\Gamma \vdash_I \kappa : t$ is trivial.
Otherwise, let us consider one of the premise $\Gamma, x : t_j \vdash_I \kappa : s_j$. As $x \notin \text{fv}(\kappa)$, this derivation does not use the rule $[\text{Ax-INT}]$ on $x$. Thus, we can easily transform it into a derivation of $\Gamma \vdash_I \kappa : s_j$.

25 If the derivation $\Gamma \vdash_I \lambda x.(\text{bind } y = x \text{ in } \kappa) : t$ uses the rule $[\text{V}_1-\text{INT}]$ for the bind, then the transformation into a derivation for $\Gamma \vdash_I \lambda x.(\kappa\{x/y\}) : t'$ is trivial.
Otherwise, we can use the following transformation:

$$ \begin{array}{c} (\forall j \in J) \\ \frac{[\text{Ax-INT}]}{[\text{V}_2-\text{INT}]} \frac{A_{j,k}}{\Gamma, x : t_j \vdash_I x : \bigvee_{k \in K_j} t'_{j,k}} \frac{A_{j,k}}{\Gamma, x : t_j, y : t'_{j,k} \vdash_I \kappa : s'_{j,k}} \\ \frac{\Gamma, x : t_j \vdash_I \text{bind } y = x \text{ in } \kappa : \bigvee_{k \in K_j} s'_{j,k} \approx s_j}{[\to I-\text{INT}}} \qquad \Gamma \vdash_I \lambda x.(\text{bind } y = x \text{ in } \kappa) : \bigwedge_{j \in J} t_j \to s_j \approx t \end{array} $$

↓

$$ \frac{\frac{\text{Easily derived by D.20 from some of the } A_{j,k}}{\Gamma, x : u_i \vdash_I \kappa \{x/y\} : v_i \le \bigwedge \{s_j \mid j \in J \text{ s.t. } u_i \le t_j\}}}{\Gamma \vdash_I \lambda x.(\kappa\{x/y\}) : \bigwedge_{i \in I} u_i \to v_i \le t} \qquad \text{with } \{u_i\}_{i \in I} = \text{partition}(\{t_j\}_{j \in J} \cup \{t'_{j,k} \mid j \in J, k \in K_j\}) $$

26 This case is similar to the case 23.

27 For the sake of simplicity, we will consider a simplified version of this rule: $\lambda x.(\text{bind } y = a \text{ in } \kappa) \dashv\vdash \text{bind } y = a \text{ in } \lambda x.\kappa$. The regular rule can then easily be deducted from that by adding a top-level binding on both sides:
$$ \text{bind } x_0 = \lambda x.(\text{bind } y = a \text{ in } \kappa) \text{ in } \kappa_0 \dashv\vdash \text{bind } x_0 = (\text{bind } y = a \text{ in } \lambda x.\kappa) \text{ in } \kappa_0 $$
and then applying the property D.24 on the right side.
If the derivation $\Gamma \vdash_I \lambda x.(\text{bind } y = \boldsymbol{a} \text{ in } \boldsymbol{\kappa}) : t$ uses the rule $[\vee_1\text{-INT}]$ for the bind, then the transformation into a derivation for $\Gamma \vdash_I \text{ bind } y = \boldsymbol{a} \text{ in } \lambda x.\boldsymbol{\kappa} : t'$ is trivial.
Otherwise, we can use the following transformation:

$$ \begin{array}{c} (\forall j \in J) \\ \frac{\displaystyle\frac{A_j}{\Gamma, x : t_j \vdash_I \boldsymbol{a} : \bigvee_{k \in K_j} t'_{j,k}} \qquad \frac{B_{j,k}}{\Gamma, x : t_j, y : t'_{j,k} \vdash_I \boldsymbol{\kappa} : s'_{j,k}}}{[\vee_2\text{-INT}]} \qquad \frac{\Gamma, x : t_j \vdash_I \text{ bind } y = \boldsymbol{a} \text{ in } \boldsymbol{\kappa} : \bigvee_{k \in K_j} s'_{j,k} \approx s_j}{[\to I\text{-INT}]} \qquad \frac{\Gamma \vdash_I \lambda x.(\text{bind } y = \boldsymbol{a} \text{ in } \boldsymbol{\kappa}) : \bigwedge_{j \in J} t_j \to s_j \approx t}{\downarrow} \end{array} $$

$$ \frac{\text{Easily derived from any of the } A_j}{\Gamma \vdash_I \boldsymbol{a} : \bigvee_{i \in I} u_i} $$

$$ \begin{array}{c} \frac{}{[\to I\text{-INT}]} \quad (\forall j \in J) \quad \frac{\displaystyle\frac{\Gamma, y : u_i, x : t_j \vdash_I \boldsymbol{\kappa} : v_{i,j} \leq s_j}{\Gamma, y : u_i \vdash_I \lambda x.\boldsymbol{\kappa} : \bigwedge_{j \in J} t_j \to v_{i,j} \leq t}}{[\vee_2\text{-INT}]} \quad \frac{}{\Gamma \vdash_I \text{ bind } y = \boldsymbol{a} \text{ in } \lambda x.\boldsymbol{\kappa} : \bigvee_{i \in I} \bigwedge_{j \in J} t_j \to v_{i,j} \leq t} \\ \text{with } \{u_i\}_{i \in I} = \text{partition}(\{t'_{j,k} \mid j \in J, k \in K_j\}) \end{array} $$

The general case (where the rule can apply under an arbitrary context) can be deduced by an application of the lemma D.26. □

PROPERTY D.30. Let $\kappa_1, \kappa_2$ such that $\kappa_1 \dashv_k \kappa_2$. If $\Gamma \vdash_I \kappa_1 : t$ then $\Gamma \vdash_I \kappa_2 : t' \leq t$.

PROOF. Immediate application of D.27 and D.29. □

PROPERTY D.31. If $\kappa \dashv_k \kappa'$, then $[\kappa] \equiv_\alpha [\kappa']$.

PROOF. Straightforward: the proof is similar to the one of D.28. □

PROPERTY D.32 (NORMALIZATION). There is no infinite chain $\kappa_1 \dashv_k \kappa_2 \dashv_k \dots$.

PROOF. Let's suppose such an infinite chain exists.

Let $n$ be the maximal number of nested lambdas in $\kappa_1$. We call depth of a binding the number of nested lambdas it is into (the depth of a binding of $\kappa_1$ is at most $n$). Let $N_\kappa(i)$ be the number of bindings of depth $i$ in an expression $\kappa$.

Let $S(\kappa)$ be the following n-uplet: $(N_\kappa(n), N_\kappa(n-1), \dots, N_\kappa(0))$. Then, the chain $S(\kappa_1), S(\kappa_2), \dots$ is strictly decreasing with respects to the lexical order, which is impossible. □

LEMMA D.33. If $\kappa \dashv_k$, then $\kappa$ satisfies the properties 1, 3 and 4 of MSC-forms, and satisfies this weaker version of property 2 (aliasing):
if bind $x = \boldsymbol{a}$ in $\boldsymbol{\kappa}'$ is a sub-expression of $\boldsymbol{\kappa}$, then $\boldsymbol{a}$ is either not a variable or a variable in $fv(\boldsymbol{\kappa})$.

PROOF. Let us start with the property 3 (extrusion of bindings). We assume that there exists a subexpression $\lambda x. \kappa_1$ of $\kappa$ and a subexpression bind $y = \boldsymbol{a}$ in $\kappa_2$ of $\kappa_1$ such that $fv(\boldsymbol{a}) \subseteq fv(\lambda x. \kappa_1)$. Then, the definition $\boldsymbol{a}$ cannot depend on any variable defined inside $\lambda x. \kappa_1$ (including $x$), otherwise this variable would be in $fv(\boldsymbol{a})$ and not in $fv(\lambda x. \kappa_1)$. Thus, we can reorder the binding $y$ in the first
position of its containing lambda-abstraction, and then apply the rule 27 on it, which contradicts $\kappa \vdash \kappa_\kappa$.

Now let's assume that there are two bindings with the definitions $a_1$ and $a_2$ such that $[a_1] \equiv_\alpha [a_2]$. By structural induction on the context of these two bindings, we can easily find two bindings with the definitions $a'_1$ and $a'_2$ such that $a'_1 \equiv_\alpha a'_2$. As we know that the property 3 is satisfied, we know that every binding is located in the body of the outermost lambda-abstraction possible (or at top-level), depending on the free variables of its definition. This means that our two definitions of $a'_1$ and $a'_2$ are not separated by a lambda-abstraction. Thus, we can reorder them to be the one next to the other, and then we can apply the rule 23 on them, which contradicts $\kappa \vdash \kappa_\kappa$. Thus, the property 1 is also satisfied.

The property 4 is trivial: any binding that does not satisfy this property can directly be eliminated with the rule 24.

We finish with the weaker version of the property 2. Let us assume that there is a binding bind $x = y$ in $\kappa'$ with $y \notin$ fv($\kappa$). It means that there exists a lambda abstraction or a binding that introduce the variable $y$. As the property 3 is satisfied, we know that these two variables are not separated by a lambda-abstraction, and thus we can reorder them to be the one next to the other. We can then apply the rule 26 or 25 depending whether $y$ is introduced by a binding or a lambda-abstraction, which contradicts $\kappa \vdash \kappa_\kappa$. □

**COROLLARY D.34.** If $\kappa \vdash \kappa_\kappa$ and $\kappa$ is closed ($fv(\kappa) = \emptyset$), then $\kappa$ is in MSC form.

**PROOF.** Direct application of D.33. □

**PROPERTY D.35 (CONFLUENCE).** Let $\kappa_1, \kappa'_1, \kappa_2$ and $\kappa'_2$ such that $\kappa_1 \equiv_\kappa \kappa'_1, \kappa_1 \vdash_\kappa \kappa_2$ and $\kappa'_1 \vdash_\kappa \kappa'_2$. Then, there exists $\kappa_3$ and $\kappa'_3$ such that $\kappa_3 \equiv_\kappa \kappa'_3, \kappa_2 \vdash_\kappa^* \kappa_3$ and $\kappa'_2 \vdash_\kappa^* \kappa'_3$.

**PROOF.** Immediate application of D.32 (normalization), D.33 (terms that cannot be rewritten using $\vdash\vdash$ are in MSC-form) and D.25 (equivalence of MSC-forms). □

**LEMMA D.36.** Let $\Gamma, e$ and $t$ such that $\Gamma \vdash e : t$. Let $\rho$ be a substitution that associates to each variable in $fv(e)$ a new (unique) name. Let $C$ be a context that defines, for each variable $x$ in $fv(e)$, the binding $bind\rho(x) = x$ in ... (it defines an alias for all variables in $fv(e)$).

Then, there exists $\kappa$ an expression in MSC-form and $t'$ a type such that $[C[\kappa]] \equiv_\alpha [e], \Gamma \vdash_C [\kappa\rho] : t'$ and $t' \le t$. Note that all possible such expressions $C[\kappa\rho]$ are equivalent with respect to $\equiv_\kappa$.

**PROOF.** From $\Gamma \vdash e : t$, we apply D.24 and D.21 so that we get $\kappa$ such that $[\kappa] = [e]$ and $\Gamma \vdash_C \kappa : t' \le t$.

Then we apply D.30, D.31 and D.33 to get $C'$ and $\kappa'$ such that $[C'[\kappa')] = [e]$ and $\Gamma \vdash_C C'[\kappa'] : t'' \le t$, with $\kappa'$ an MSC-form and $C'$ a context that optionally defines an alias for some variables in $fv(e)$.

We can easily derive $\Gamma \vdash_C [(C'[\kappa'])\rho] : t'' \le t$ from that just by applying $\rho$ to the derivation tree and by adding additional aliases at top-level for the new variables in $\rho$ (these additional bindings can be typed using $[\nu_1-INT]$ when the aliased variable is not in $\Gamma$, and otherwise using $[\nu_2-INT]$ with $J$ a singleton).

Now, we can derive $\Gamma \vdash_C [\kappa'\rho] : t''' \le t$ by merging the aliases defined by $C'$ and those defined by $C$ using the rule 26 (see lemma D.29).

Finally, note that for a given $C$ such as in the statement of the lemma, all the expressions $C[\kappa'\rho]$ with $\kappa'$ a MSC-form such that $[C[\kappa'\rho]] = [e]$ are equivalent with respect to $\equiv_\kappa$ (quite straightforward by using D.25). □

**THEOREM D.37 (COMPLETENESS OF THE MSC FORM).** If $\vdash_C e : t$ and if $\kappa$ is a maximal sharing canonical form such that $[\kappa] \equiv_\alpha [e]$, then $\exists t' \text{ such that } t' \le t \text{ and } \vdash_C \kappa : t'$.
**PROOF.** Direct application of D.36. □

**THEOREM D.38 (COMPLETENESS OF THE INTERMEDIATE TYPE SYSTEM).** If $\Gamma \vdash e : t$ then $\exists e', t' \text{ such that } [e'] \equiv_\alpha e, t' \le t$, and $\Gamma \vdash_I e' : t'$

**PROOF.** We apply all the normalization lemmas D.5, D.6, D.7 and D.8 to the derivation of the judgement $\Gamma \vdash e : t$, and we proceed by structural induction on it.

Depending on the last rule used (we use the variable names defined in this rule):

[CONST] Trivial.

[Ax] Trivial.

[≤] Trivial (by induction on the premise).

[→I] By induction (application of the rule [→I-INT] with $J = \{t_1\}$).

[→E] By induction on the premises, we get $\Gamma \vdash_I e_1 : s_1 \le t_1 \to t_2$ and $\Gamma \vdash_I e_2 : s_2 \le t_1$ with $[e_1] \equiv_\alpha e_1$ and $[e_2] \equiv_\alpha e_2$. According to the definition of ◦ (and by monotonicity), we have $s_1 \circ s_2 \le (t_1 \to t_2) \circ t_1 \le t_2$. Thus, we can conclude with an application of the rule [→E-INT].

[×I] By induction (application of the rule [×I-INT]).

[×E₁] By induction on the premise, we get $\Gamma \vdash_I e : s \le t_1 \times t_2$ with $[e] \equiv_\alpha e$. According to the definition of $\pi_1$ (and by monotonicity), we have $\pi_1 s \le \pi_1 (t_1 \times t_2) \le t_1$. Thus, we can conclude with an application of the rule [×E-INT].

[×E₂] Similar to the previous case.

[∧+] Thanks to the lemma D.6, we know that the premises of this rule are applications of [→I]. Moreover, by induction, we have $\forall i \in I. \Gamma \vdash_I e_i : t'_i \le t_i$ with $[e_i] \equiv_\alpha e$. By applying the lemma D.36, we can derive $\forall i \in I. \Gamma \vdash_I \kappa : t'_i \le t_i$ with $[\kappa] \equiv_\alpha e$ and $\kappa$ being a MSC-form preceded by some aliasing. We can conclude with an application of the rule [→I-INT] with $J = I$.

[∨+] We have $e = e_\circ\{e'/x\}$. By induction on the premises, we have $\Gamma \vdash_I e' : t' \le \bigvee_{i \in I} t_i$ with $[e'] \equiv_\alpha e'$ and $\forall i \in I. \Gamma, x : t_i \vdash_I e_i : s_i \le t$ with $\forall i \in I. [e_i] \equiv_\alpha e_\circ$.

By applying the lemma D.36, we can derive $\forall i \in I. \Gamma, x : t_i \vdash_I \kappa : s'_i \le s_i \le t$ with $[\kappa] \equiv_\alpha e_\circ$ and $\kappa$ being a MSC-form preceded by some aliasing.

By monotonicity (D.19), we have $\forall i \in I. \Gamma, x : (t_i \wedge t') \vdash_I \kappa : s''_i \le t$.

Let us consider the intermediate expression $e = \text{bind } x = e' \text{ in } \kappa$. We have $[e'] \equiv_\alpha e$. Moreover, we can derive $\Gamma \vdash e : \bigvee_{i \in I} s''_i \le t$ by using the rule [V₂-INT].

[0] By induction (application of the rule [0-INT]).

$[\in_1]$ By induction (application of the rule $[\in_1-\text{INT}$]).

$[\in_2]$ By induction (application of the rule $[\in_2-\text{INT}$]).

□
## D.3 Algorithmic Type System

See 4 for the full intermediate system and A.9 for the full algorithmic system.

**THEOREM D.39 (SOUNDNESS OF THE ALGORITHMIC TYPE SYSTEM).** If $\Gamma \vdash_I \kappa : t$ then $\Gamma \vdash_I \langle \kappa \rangle : t$.

**PROOF.** This direction is trivial: all the rules of the algorithmic system have an equivalent in the intermediate system. For the rules $[\vee_2\text{-INT}]$ and $[\to\text{-I-INT}]$, the splits $\{t_j\}_{j \in J}$ to choose correspond to the ones determined by the annotations in the corresponding rule $[\vee_2\text{-ALG}]$ or $[\to\text{-I-ALG}]$. $\square$

**LEMMA D.40.** If $\Gamma \vdash_I e : t$, then there exists a derivation of $\Gamma \vdash_I e : t' \le t$ such that, for every application of a rule $[\to\text{-I-INT}]$ or $[\vee_2\text{-I-INT}]$, the set of types $\{t_j\}_{j \in J}$ is disjoint ($\forall j, j' \in J. j \neq j' \Rightarrow t_j \land t_j$).

**PROOF.** Let us suppose there is an application of $[\to\text{-I-INT}]$ or $[\vee_2\text{-INT}]$ that uses a set of types $\{t_j\}_{j \in J}$ that does not satisfy the property. We will transform the derivation so that a new set of disjoint types $\{t'_j\}_{j \in J'}$ will be used instead.

Let us consider $\{t'_j\}_{j \in J'} = \text{partition}(\{t_j\}_{j \in J})$. These types are disjoint and cover the same domain as before. Moreover, by monotonicity (D.19) and by using the lemma D.20, we can derive $\forall j' \in J'. \Gamma, x : t'_{j'} \vdash_I \kappa : s'_{j'} \le \bigwedge_{j \in J \text{ s.t. } s'_{j'} \le s_j} s_j$ from all the derivations $\forall j \in J. \Gamma, x : t_j \vdash_I \kappa : s_j$. Thus, we can update our application of $[\to\text{-I-INT}]$ or $[\vee_2\text{-I-INT}]$ so that it uses the set of types $\{t'_j\}_{j \in J'}$. It might give a smaller resulting type, but by monotonicity we will still be able to deduce $\Gamma \vdash_I e : t' \le t$.

Note that this transformation does not compromise the disjointness of the types of the other applications of $[\to\text{-I-INT}]$ and $[\vee_2\text{-I-INT}]$, thus we can apply it multiple times until all the rules $[\to\text{-I-INT}]$ and $[\vee_2\text{-I-INT}]$ use disjoint types. $\square$

**THEOREM D.41 (COMPLETENESS OF THE ALGORITHMIC TYPE SYSTEM).** If $\kappa$ is a MSC-form and $\Gamma \vdash_I \kappa : t$, then $\exists \kappa$ such that $\langle \kappa \rangle = \kappa$ and $\Gamma \vdash_{\vdash_I \kappa} t' \le t$

**PROOF.** Note that the only difference between the algorithmic system and the intermediate one is that the set of splits $\{t_j\}_{j \in J}$ in the rules $[\to\text{-I-ALG}]$ and $[\vee_2\text{-ALG}]$ and the choice of whether to use the rule $[\vee_1\text{-ALG}]$ or $[\vee_2\text{-ALG}]$ are determined by the annotations contained in $\kappa$. Thus, the challenge here will be to annotate $\kappa$ so that it allows to "replay" the derivation tree of $\Gamma \vdash_I \kappa : t$ with the algorithmic rules.

First, we apply the transformation of the lemma D.40 to the derivation of $\Gamma \vdash_I \kappa : t$ so that we get a derivation $D$ of $\Gamma \vdash_I \kappa : t' \le t$ that satisfies the property described in the statement of this lemma.

Now, we start from an algorithmic expression $\kappa$ similar to $\kappa$ but with every binding and lambda annotated by an empty annotation. Each time a rule $[\to\text{-I-INT}]$ is applied in the derivation $D$ (with $\Gamma \vdash_I \lambda x.(e) : t_o$ as conclusion), we add to the annotations of $x$ the splits $\{(\Gamma \vdash t_j)\}_{j \in J}$ (with $\{t_j\}_{j \in J}$ being the set of types used by the rule). We proceed similarly for the applications of $[\vee_2\text{-INT}]$ in order to annotate the bindings.

The term $\kappa$ we obtain can be typed with the algorithmic type system: we obtain a derivation very similar to $D$ (every rule application of the derivation $D$ is replaced by a similar application of the corresponding rule of the algorithmic type system). The applications of $[\to\text{-I-ALG}]$ and $[\vee_2\text{-ALG}]$ will use the same set of types $\{t_j\}_{j \in J}$ as in the derivation $D$, because:

$\supset$ We have added the annotations $\{\Gamma \vdash t_j\}_{j \in J}$ to the corresponding variable

$\subseteq$ Only these annotations will be selected: the annotations we might have added to this variable because of the other applications of $[\vee_2\text{-INT}]$ or $[\to\text{-I-INT}]$ require a disjoint environment. Indeed, the different applications of $[\vee_2\text{-INT}]$ or $[\to\text{-I-INT}]$ for a given variable are in different branches and all branches use a disjoint environment $\Gamma$ thanks to the lemma D.40.
<figure><img src="image_7.png" /></figure>

## D.4 Annotations Reconstruction Algorithm

See B.3 for the full annotations reconstruction algorithm.

We define the following function:

$$ \mathit{filter}_{\Gamma}(A) = \{(\Gamma' \triangleright t') | (\Gamma' \triangleright t') \in A, \Gamma' \leq \Gamma\} $$

We extend this function so that it can take an algorithmic expression $\varphi$ as argument and returns the same expression $\varphi$ where every annotation A has been replaced by $\mathit{filter}_{\Gamma}(A)$.

**LEMMA D.42.** If $\Gamma \vdash_R \varphi : t \Rightarrow \{\mathit{filter}_\Gamma(\varphi), \{\Gamma\}\}$ then $\Gamma \vdash_R \mathit{filter}_\Gamma(\varphi) : t' \leq t$.

**PROOF.** For convenience, let us define $\varphi' = \mathit{filter}_\Gamma(\varphi)$. We proceed by induction on the derivation tree of $\Gamma \vdash_R \varphi : t \Rightarrow \{\varphi', \{\Gamma\}\}$.

**[CONST]** We trivially have $\Gamma \vdash_R \varphi' : b_c \leq t$.

**[CONSTUNTYPABLE]** Impossible (it cannot return $\{\varphi', \{\Gamma\}\}$).

**[PROJEMPTY]** We trivially have $\Gamma \vdash_R \varphi' : \emptyset \leq t$.

**[PROJ1]** We know that $\{\Gamma[x : \triangleq t_i \times s_i]\}_{i \in I} = \{\Gamma\}$. In particular, it means that $\Gamma \in \{\Gamma[x : \triangleq t_i \times s_i]\}_{i \in I}$ and thus $\exists i \in I. \Gamma(x) \leq t_i \times s_i$. As $\forall i \in I. t_i \times s_i \leq (t \times 1)$, we can derive $\Gamma \vdash_R \varphi' : t' \leq t$.

**[PROJ2]** Similar to the previous case.

**[PAIREMPTY]** We trivially have $\Gamma \vdash_R \varphi' : \emptyset \leq t$.

**[PAIR]** We know that $\{\Gamma[x_1 : \triangleq t_i][x_2 : \triangleq s_i]\}_{i \in I} = \{\Gamma\}$. In particular, it means that $\Gamma \in \{\Gamma[x_1 : \triangleq t_i][x_2 : \triangleq s_i]\}_{i \in I}$ and thus $\exists i \in I. \Gamma(x_1) \leq t_i$ and $\Gamma(x_2) \leq s_i$. As $\forall i \in I. t_i \times s_i \leq t$, we can derive $\Gamma \vdash_R \varphi' : t' \leq t$.

**[CASEEMPTY]** We trivially have $\Gamma \vdash_R \varphi' : \emptyset \leq t$.

**[CASE]** We know that $\{\Gamma[x : \triangleq s][x_1 : \triangleq t], \Gamma[x : \triangleq \neg s][x_2 : \triangleq t]\} = \{\Gamma\}$. In particular, it means that $\Gamma \in \{\Gamma[x : \triangleq s][x_1 : \triangleq t]\}$ or $\Gamma \in \{\Gamma[x : \triangleq \neg s][x_2 : \triangleq t]\}$. Let's consider the first case. We can deduce $\Gamma(x) \leq s$ and $\Gamma(x_1) \leq t$, and thus we have $\Gamma \vdash_R \varphi' : t' \leq t$ (rule $\epsilon_1$-ALG). The second case is similar (rule $\epsilon_2$-ALG).

**[APPRE]** We trivially have $\Gamma \vdash_R \varphi' : \emptyset \leq t$.

**[APPLEEMPTY]** We trivially have $\Gamma \vdash_R \varphi' : \emptyset \leq t$.

**[APPR]** We know that $\{\Gamma[x_1 : \triangleq (s_i \wedge \Gamma(x_2)) \to t][x_2 : \triangleq s_i]\}_{i \in I} = \{\Gamma\}$. In particular, it means that $\Gamma \in \{\Gamma[x_1 : \triangleq (s_i \wedge \Gamma(x_2)) \to t][x_2 : \triangleq s_i]\}_{i \in I}$ and thus $\exists i \in I. \Gamma(x_1) \leq (s_i \wedge \Gamma(x_2)) \to t$ and $\Gamma(x_2) \leq s_i$. We can deduce that $\Gamma(x_1) \leq \Gamma(x_2) \to t$ and thus we can derive $\Gamma \vdash_R \varphi' : t' \leq t$.

**[APPL]** If this rule apply, then we know that [APPR] cannot apply and thus either:

* $\Gamma(x_1) \not\leq \emptyset \to 1$, in this every $s_i$ is a strict refinement of $\Gamma(x_1)$ and thus the rule cannot return $\{\varphi', \{\Gamma\}\}$, or

* The DNF of $\Gamma(x_1)$ is a disjunction of at least 2 elements, in this case we know by minimality of the DNF that every $s_i$ is a strict refinement of $\Gamma(x_1)$ and thus the rule cannot return $\{\varphi', \{\Gamma\}\}$, or

* The DNF of $\Gamma(x_1)$ is a disjunction of 0 element and thus the rule will return $\{\varphi', \{\}\}$
  In any case it is impossible for the rule to return $\{\varphi', \{\Gamma\}\}$.

**[Abs]** In order for this rule to return $\{\varphi', \{\Gamma\}\}$, we must have:

* $A' = \mathit{filter}_\Gamma(A)$: We can deduce that $(\Gamma \triangleright A) = \{s_i\}_{i \in I}$ and that $\forall i \in I. \Gamma_i = \{(\Gamma, x : s_i)\}$.

* $\mathit{merge}_\kappa(\{\kappa_i\}_{i \in I}) = \mathit{filter}_\Gamma(\kappa)$: We can deduce that $\forall i \in I. \kappa_i = \mathit{filter}_{(\Gamma, x: s_i)}(\kappa)$.

* $\cup_{i \in I} \Gamma'_i = \{\Gamma\}$: (nothing more to deduce)
Thus, by induction, we can deduce $\forall i \in I. \Gamma, x : s_i \vdash_A \kappa_i : t'_i \le t \circ_1 s_i$. As $\text{dom}(t) = \bigvee_{j \in J} s_j \le \bigvee (\Gamma \triangleright A) \le \bigvee_{i \in I} s_i$, we have $\wedge s_i \rightarrow (t \circ_1 s_i) \le t$. Consequently, we can derive $\Gamma \vdash_A \varphi' : t' \le t$ (rule [→I-ALG]).

Note that the final check $\bigvee_{j \in J} s_j \le \bigvee\{s' | (\Gamma' \triangleright s') \in A'\}$ of the [Abs] rule is not strictly needed for the soundness, but it helps to detect an impossibility to obtain the type $t$ sooner by checking if its domain can possibly be covered with the new annotations.

[**AbsUNTYPEABLE**] Impossible (it cannot return {$\varphi', \{\Gamma\}$}).

[**UNDEFINEDVAR**] Impossible (it cannot return {$\varphi', \{\Gamma\}$}).

[**BINDARGSKIP**] In order for this rule to return {$\varphi', \{\Gamma\}$}, it is necessary to have $\kappa' = \text{filter}_\Gamma(\kappa)$ as well as $\Gamma' = \{\Gamma\}$. Thus, by induction on the second premise, we get $\Gamma \vdash_A \kappa' : t' \le t$. With a simple application of the $[\vee_1\text{-ALG}]$ rule, we can derive $\Gamma \vdash_A \varphi' : t' \le t$.

[**BINDARGUNTYPE**] Similar to the previous case.

[**BINDARGREFENV**] Impossible (it cannot return {$\varphi', \{\Gamma\}$} because $\Gamma' \neq \{\Gamma\}$).

[**BINDARGREFANNS**] Impossible (it cannot return {$\varphi', \{\Gamma\}$} because $a' \neq a$).

[**BIND**] In order for this rule to return {$\varphi', \{\Gamma\}$}, we must have:

* $\bigcup_{i \in I} A_i = \text{filter}_\Gamma(A)$: We can deduce that $(\Gamma \triangleright A) = \{s_i\}_{i \in I}$ and that $\forall i \in I. \Gamma' = \{((\Gamma, x : s_i))\}$. This implies $\forall i \in I. \Gamma' = \{((\Gamma, x : s_i))\}$ because propagate can only refine environments.

* $\text{merge}_\kappa(\{\kappa_i\}_{i \in I}) = \text{filter}_\Gamma(\kappa)$: We can deduce that $\forall i \in I. \kappa_i = \text{filter}_{(\Gamma, x:s_i)}(\kappa)$.

* $\bigcup_{i \in I} \Gamma'_i = \{\Gamma\}$: (nothing more to deduce)

Thus, by induction, we can deduce $\forall i \in I. \Gamma, x : s_i \vdash_A \kappa_i : t'_i \le t$. Consequently, we can derive $\Gamma \vdash_A \varphi' : t' \le t$ (rule $[\vee_2\text{-ALG}]$).

[**VAR**] We know that $\{\Gamma[x : \begin{array}{l} \triangleq \\ \Gamma \end{array}]\} = \{\Gamma\}$. We can deduce $\Gamma(x) \le t$ and thus we trivially have $\Gamma \vdash_A \varphi' : t' \le t$.

□

**THEOREM D.43 (SOUNDNESS OF THE RECONSTRUCTION ALGORITHM).** If $\kappa$ is a closed MSC-form and $\mathcal{R}(\kappa) = \kappa'$, then $\emptyset \vdash_A \kappa' : t$ for some $t$.

**PROOF.** Immediate corollary of the previous lemma D.42. □