## H.3 Split Propagation System

The split propagation system defined in this section tries to deal with the following problem: given an environment $\Gamma$, an atom $a$ and a type $t$, what additional assumptions can be made on $\Gamma$ in order to ensure that $a$ has type $t$? It is used by the main reconstruction system in order to propagate splits made by bindings.

$$ [\text{CONST}_1] \quad \frac{b_c \le \mathbf{u}}{\Gamma \vdash_{\mathcal{E}} (c : \mathbf{u}) \Rightarrow \emptyset} $$

$$ [\text{CONST}_2] \quad \overline{\Gamma \vdash_{\mathcal{E}} (c : \mathbf{u}) \Rightarrow \emptyset} $$

$$ [\text{Ax}_1] \quad \frac{\Gamma(x) \le \mathbf{u}}{\Gamma \vdash_{\mathcal{E}} (x : \mathbf{u}) \Rightarrow \emptyset} $$

$$ [\text{Ax}_2] \quad \overline{\Gamma \vdash_{\mathcal{E}} (x : \mathbf{u}) \Rightarrow \emptyset} $$

$$ [\text{PROJ}_1] \quad \overline{\Gamma \vdash_{\mathcal{E}} (\pi_1 x : \mathbf{u}) \Rightarrow \{\{x : \mathbf{u} \times \mathbf{1}\}\}} $$

$$ [\text{PROJ}_2] \quad \overline{\Gamma \vdash_{\mathcal{E}} (\pi_2 x : \mathbf{u}) \Rightarrow \{\{x : \mathbf{1} \times \mathbf{u}\}\}} $$

$$ [\text{PAIR}] \quad \frac{\mathbf{u} \stackrel{\text{DNF}}{\cong} (\bigvee_{i \in I} (\mathbf{u}_i \times \mathbf{v}_i)) \lor \dots}{\Gamma \vdash_{\mathcal{E}} ((x_1, x_2) : \mathbf{u}) \Rightarrow \{\{x_1 : \mathbf{u}_i\} \land \{x_2 : \mathbf{v}_i\} \mid i \in I\}} $$

$$ [\text{CASE}] \quad \overline{\Gamma \vdash_{\mathcal{E}} ((x \in \tau) ? x_1 : x_2 : \mathbf{u}) \Rightarrow \{\{x : \tau, x_1 : \mathbf{u}\}, \{x : \neg \tau, x_2 : \mathbf{u}\}\}} $$

$$ [\text{APP}] \quad \frac{\Gamma(x_1) \stackrel{\text{DNF}}{\cong} \bigvee_{i \in I} t_i \quad \forall i \in I. \{\sigma_j\}_{j \in J_i} = \text{tally}(\{t_i \le \alpha \to \mathbf{u}\})}{\Gamma \vdash_{\mathcal{E}} (x_1 x_2 : \mathbf{u}) \Rightarrow \bigcup_{i \in I} \Gamma_i} \quad \alpha \in \mathcal{V}_p \text{ fresh} $$

where, for every $i \in I$, $\Gamma_i = \{\{x_1 : (t_i \sigma_j) \sigma'_j, x_2 : (\alpha \sigma_j) \sigma'_j\} | j \in J_i\}$ with $\sigma'_j$ a type substitution mapping each polymorphic type variable $\beta$ appearing in $t_i \sigma_j$ or $\alpha \sigma_j$ to either:

* 1 if $\beta$ only appears in covariant positions in $\alpha \sigma_j$,

* 0 if $\beta$ only appears in contravariant positions in $\alpha \sigma_j$,

* a fresh monomorphic type variable otherwise.

$$ [\text{LAMBDA}] \quad \overline{\Gamma \vdash_{\mathcal{E}} (\lambda x. \kappa : \mathbf{u}) \Rightarrow \emptyset} $$

The following rules can be added to support the extensions presented in Appendix A:

$$ [\text{LET}] \quad \overline{\Gamma \vdash_{\mathcal{E}} (\text{let } x_1 \text{ in } x_2 : \mathbf{u}) \Rightarrow \{\{x_2 : \mathbf{u}\}\}} $$

$$ [\text{CONSTR}] \quad \overline{\Gamma \vdash_{\mathcal{E}} (x \otimes \tau : \mathbf{u}) \Rightarrow \{\{x : \mathbf{u}\}\}} $$

## I PROOFS

The proofs are for the source language presented in section 2 without extension:

$$ \textbf{Expressions} \quad e ::= c \mid x \mid \lambda x.e \mid ee \mid (e, e) \mid \pi_i e \mid (e \in \tau) ? e : e $$

We fix some notations relative to substitutions:

* $\phi$ ranges over substitutions from type variables ($\mathcal{V}_P \dot{\cup} \mathcal{V}_M$) to types

* $\rho$ ranges over renamings of polymorphic variables, that is, injective substitutions from $\mathcal{V}_P$ to $\mathcal{V}_P$

* $\sigma$ ranges over substitutions from polymorphic type variables $\mathcal{V}_P$ to types

* $\Sigma$ ranges over sets of substitutions from polymorphic type variables $\mathcal{V}_P$ to types

* $\psi$ ranges over substitutions from monomorphic type variables $\mathcal{V}_M$ to monomorphic types
* Ψ ranges over sets of substitutions from monomorphic type variables $V_M$ to monomorphic types

## I.1 A Canonical Form for the Derivations

Derivations for the declarative type system can have many shapes (see Appendix D for the full declarative system, without the rules for extensions). In particular, the union elimination rule [VE] can be used anywhere in the derivation and changes the expression to type by performing a substitution on it. Other non-structural rules such as [∧], [≤] and [Inst] can also be applied anywhere in the derivation. In this section, we will define canonical derivations that restrict the use of those rules. This will then be used, in Section I.2, to establish a type safety theorem.

### I.1.1 Alternative Form of the Declarative Type System.
In order to be able to express our normalisations lemmas, we first need to slightly modify some rules of the declarative type system. In order to avoid confusions, the modified declarative type system will use this turnstile symbol: ⊢.

First, we modify the [Ax] rule so that it can perform a renaming of the polymorphic type variables in $Γ(x)$:

$$[Ax] \quad \overline{\Gamma \vdash x : \Gamma(x) \rho}$$

This new [Ax] rule is derivable in the initial delcarative type system by composing a [Ax] rule and a [Inst] rule. Still, allowing the [Ax] rule to perform a renaming of polymorphic type variables is useful, as it allows to uncorrelate types without resorting to the [Inst] rule. For instance, consider the pair $(x, x)$ with $x$ having the type $\alpha \to \alpha$. While this pair could be typed $(\alpha \to \alpha) \times (\alpha \to \alpha)$, this type does not allow instantiating the left-hand side and right-hand side of the product independently. A better type would be $(\alpha \to \alpha) \times (\beta \to \beta)$, and with this new [Ax] rule, it can be derived without having to use a [Inst] rule. This way, the [Inst] rule can be reserved to cases that require non trivial instantiations (i.e. not just renamings). Note that the necessity of performing this renaming comes from the fact that we do not use type schemes $\forall \vec{\alpha}$. $t$, where renaming of the type variables in $\vec{\alpha}$ can be performed implicitly anywhere.

Secondly, we use a [∧] rule of multiple arity instead of a binary one:

$$[∧] \quad \frac{(\forall i \in I) \quad \Gamma \vdash e : t_i}{\Gamma \vdash e : \bigwedge_{i \in I} t_i} \quad I \neq \emptyset$$

This allows to combine successive [∧] rule applications into one [∧] rule, making the normalisation lemmas easier to express. This new [∧] rule is admissible in the ⊢ system: it can be replaced by several consecutive [∧] nodes.

Similarly, we will use a [∨] rule of multiple arity:

$$[∨] \quad \frac{\Gamma \vdash e' : s \quad (\forall i \in I) \quad \Gamma, x : s \wedge u_i \vdash e : t}{\Gamma \vdash e\{e'/x\} : t} \quad \{u_i\}_{i \in I} \in \mathrm{Part}(\emptyset)$$

with Part($t$) denoting the set of partitions of the type $t$, that is, the set of all sets $\{t_i\}_{i \in I}$ such that: (i) $\bigvee_{i \in I} t_i \approx t$, (ii) $\forall i \in I. t_i \neq \emptyset$, and (iii) $\forall i, j \in I. i \neq j \Rightarrow t_i \wedge t_j \approx \emptyset$. The guard condition is most of time omitted, for concision.

This allows to combine successive [∨] rule applications substituting the same sub-expression into one [∨] rule, making the normalisation lemmas easier to express. Again, this new [∨] rule is
admissible. For instance, the following derivation:

$$ [\mathbf{V}] \frac{\frac{A}{\Gamma + e' : s} \quad \frac{B}{\Gamma, y : s \wedge \mathbf{u}_1 + e : t} \quad \frac{C}{\Gamma, y : s \wedge \mathbf{u}_2 + e : t} \quad \frac{D}{\Gamma, y : s \wedge \mathbf{u}_3 + e : t}}{\Gamma + e\{e' / x\} : t} $$

can be transformed to use only two binary [V] rules:

$$ [\mathbf{V}] \frac{\frac{A}{\Gamma + e' : s} \quad \frac{B}{\Gamma, x : s \wedge \mathbf{u}_1 + e : t} \quad \frac{X}{\Gamma, x : s \wedge \neg \mathbf{u}_1 + e : t}}{\Gamma + e\{e' / x\} : t} $$

with X being the following derivation:

$$ [\mathbf{V}] \frac{\frac{C\{y/x\}}{\Gamma, x : s \wedge \neg \mathbf{u}_1, y : s \wedge \mathbf{u}_2 + e\{y/x\} : t} \quad \frac{D\{y/x\}}{\Gamma, x : s \wedge \neg \mathbf{u}_1, y : s \wedge \mathbf{u}_3 + e\{y/x\} : t}}{\Gamma, x : s \wedge \neg \mathbf{u}_1 + (e\{y/x\})\{x/y\} : t} $$

This construction can be generalized for a partition of $\mathbb{1}$ of any cardinality.

Lastly, we distinguish variables that are introduced by a $[\rightarrow I]$ node from variables introduced by a $[\mathbf{V}]$ node. The formers are called *lambda variables*, the set of all lambda variables is denoted by $\text{Vars}_\lambda$ and ranged over by $x$, $y$, and $z$. The latters are called *binding variables*, the set of all binding variables is denoted by $\text{Vars}_\beta$ and ranged over by $x$, $y$, and $z$. $\text{Vars}_\lambda$ and $\text{Vars}_\beta$ form a partition of the set of variables $\text{Vars}$ (formally, $\text{Vars} = \text{Vars}_\lambda \cup \text{Vars}_\beta$). The syntax of expressions and the rules of the type system are changed accordingly as follows:

$$ \textbf{Expressions} \quad e ::= c \mid x \mid x \mid \lambda x.e \mid ee \mid (e, e) \mid \pi_i e \mid (e \in \tau) \mid ?e : e $$

$$ [\text{Ax}_\lambda] \quad \frac{\Gamma \vdash x : \Gamma(x) \rho}{\Gamma \vdash x : \Gamma(x) \rho} \qquad [\text{Ax}_\nu] \quad \frac{\Gamma \vdash x : \Gamma(x) \rho}{\Gamma \vdash x : \Gamma(x) \rho} $$

$$ [\mathbf{V}] \frac{\frac{\Gamma + e' : s \quad (\forall i \in I) \quad \Gamma, x : s \wedge \mathbf{u}_i \vdash e : t}{\Gamma \vdash e\{e' / x\} : t}}{\{\mathbf{u}_i\}_{i \in I} \in \text{Part}(\mathbb{1})} $$

When needed, we will use the notation $x/x$ to range over both binding variables and lambda variables. For instance, we could write the proposition $\forall x/x \in \text{dom}(\Gamma)$. $\Gamma(x/x) \neq \emptyset$. We say that an expression $e$ is a ground expression if $e$ does not contain any binding variable, and that a derivation $D$ is a ground derivation if it derives a judgement for a ground expression. For what concerns programs, they use lambda variables for top-level definitions, and are only composed of ground expressions.

This new system is equivalent to the initial type system: the combination of both $[\text{Ax}_\lambda]$ and $[\text{Ax}_\nu]$ gives the previous $[\text{Ax}]$ rule.

A full declarative type system with these modifications is presented in Figure 4.

The rules $[\text{CONST}]$, $[\text{Ax}_\lambda]$, $[\rightarrow I]$, $[\rightarrow E]$, $[\times I]$, $[\times E_1]$, $[\times E_2]$, $[\emptyset]$, $[\epsilon_1]$ and $[\epsilon_2]$ will be called *structural rules* as their use is guided by the structure of the expression to type, each of them allowing to type a specific syntactic construction. In particular, note that the rule $[\text{Ax}_\nu]$ is not considered structural as binding variables $x$ are not supposed to appear in the initial expression (they are only introduced in the derivation when using a $[\mathbf{V}]$ rule).

Also, the first premise of a $[\mathbf{V}]$ rule will be called its *definition premise*, and its others premises will be called *body premises*.

All the proofs in the next sections and chapters will use the $\vdash$ declarative type system, which is equivalent to the $\vdash$ type system.
$$ [\text{CONST}] \quad \overline{\Gamma \vdash c : b_c} \qquad [\text{Ax}_\lambda] \quad \overline{\Gamma \vdash x : \Gamma(x)\rho} \qquad [\text{Ax}_\nu] \quad \overline{\Gamma \vdash x : \Gamma(x)\rho} \\ \qquad \quad [\to I] \quad \frac{\Gamma, x : \mathbf{u} \vdash e : t}{\Gamma \vdash \lambda x.e : \mathbf{u} \to t} \qquad \quad [\to E] \quad \frac{\Gamma \vdash e_1 : t_1 \to t_2 \quad \Gamma \vdash e_2 : t_1}{\Gamma \vdash e_1 e_2 : t_2} $$

$$ [\times I] \quad \frac{\Gamma \vdash e_1 : t_1 \quad \Gamma \vdash e_2 : t_2}{\Gamma \vdash (e_1, e_2) : t_1 \times t_2} \qquad [\times E_1] \quad \frac{\Gamma \vdash e : t_1 \times t_2}{\Gamma \vdash \pi_1 e : t_1} \qquad [\times E_2] \quad \frac{\Gamma \vdash e : t_1 \times t_2}{\Gamma \vdash \pi_2 e : t_2} $$

$$ [\emptyset] \quad \frac{\Gamma \vdash e : \emptyset}{\Gamma \vdash (e \in \tau) ? e_1 : e_2 : \emptyset} \qquad [\in_1] \quad \frac{\Gamma \vdash e : \tau \quad \Gamma \vdash e_1 : t_1}{\Gamma \vdash (e \in \tau) ? e_1 : e_2 : t_1} \qquad [\in_2] \quad \frac{\Gamma \vdash e : \neg \tau \quad \Gamma \vdash e_2 : t_2}{\Gamma \vdash (e \in \tau) ? e_1 : e_2 : t_2} $$

$$ [\lor] \quad \frac{\Gamma \vdash e' : s \quad (\forall i \in I) \quad \Gamma, x : s \wedge \mathbf{u}_i \vdash e : t}{\Gamma \vdash e\{e' / x\} : t} \qquad \{\mathbf{u}_i\}_{i \in I} \in \text{Part}(\emptyset) $$

$$ [\land] \quad \frac{(\forall i \in I) \quad \Gamma \vdash e : t_i \quad I \neq \emptyset}{\Gamma \vdash e : \bigwedge_{i \in I} t_i} \qquad [\text{INST}] \quad \frac{\Gamma \vdash e : t}{\Gamma \vdash e : t \sigma} \qquad [\le] \quad \frac{\Gamma \vdash e : t}{\Gamma \vdash e : t'} \quad t \le t' $$

<caption>Fig. 4. Alternative Declarative Type System</caption>

**PROPOSITION I.1.** For any ground expression *e*, type environment $\Gamma$ and type *t*:

$$ \Gamma \vdash e : t \Leftrightarrow \Gamma \vdash e : t $$

**PROOF.** The $\Rightarrow$ direction is trivial. The $\Leftarrow$ direction is obtained by using 
 nodes to rename polymorphic type variables of axioms whenever needed, and by locally transforming *n*-ary $[\wedge]$ nodes into *n* − 1 binary $[\wedge]$ nodes, and *n*-ary $[\vee]$ nodes into *n* − 1 binary $[\vee]$ nodes, as detailed above. $\square$

Now, we introduce a new order $\le_P$ on types. Intuitively, it adds to the subtyping order $\le$ the possibility to instantiate polymorphic type variables. We then use it in the statement of a monotonicity lemma that will be used extensively in the next sections.

**DEFINITION I.2 (POLYMORPHIC SUBTYPING ORDER).** We define the order relation $\le_P$ over types as follows:

$$ \forall t_1, t_2. \ t_1 \le_P t_2 \Leftrightarrow \exists \Sigma. \ t_1 \Sigma \le t_2 $$

Note that, while this order will be extensively used in the proofs, it will not be used in algorithms as we have no way to compute it. Indeed, while deciding this order might seem equivalent to solving a tallying problem (defined in Section 4.1), it is actually not the case as deciding this order requires to find a set of substitutions $\Sigma$, and not a single substitution $\sigma$.

**DEFINITION I.3.** For any order relation $\le$ over types, we define the order relation $\le$ over environments as follows:

$$ \forall \Gamma_1, \Gamma_2. \ \Gamma_1 \le \Gamma_2 \Leftrightarrow \forall x/\Sigma \in \operatorname{dom}(\Gamma_2). \ x/\Sigma \in \operatorname{dom}(\Gamma_1) \text{ and } \Gamma_1(x) \le \Gamma_2(x) $$
We introduce for convenience a new notation that takes the form of a new rule `[INST∧≤]`, but is actually just a shortand for a specific combination of `
`, `[^]`, and `[≤]` rules:

$$ [\text{INST} \wedge \leq] \frac{\frac{A}{\Gamma \vdash e : t'} \quad (\exists \Sigma. \ \Lambda_{\sigma \in \Sigma} t' \sigma \leq t)}{\Gamma \vdash e : t} \quad \leftrightarrow \quad [\leq] \frac{\frac{A}{[\text{INST}] \quad \frac{\Gamma \vdash e : t'}{\Gamma \vdash e : t' \sigma}} \quad \forall \sigma \in \Sigma}}{\Gamma \vdash e : \Lambda_{\sigma \in \Sigma} t' \sigma} $$

**LEMMA I.4 (MONOTONICITY).** For derivation *D* of Γ+e:t and environment Γ' such that Γ' ≤ₚ Γ, *D* can be transformed into a derivation of Γ'+e:t just by adding `[≤]`, `
` and `[^]` nodes.

**PROOF.** Straightforward induction on the derivation Γ+e:t, where each `[Ax_ν]` and `[Ax_λ]` node is replaced by a `[INST∧≤]` pattern of that node. □

I.1.2 Normalisation Lemmas. Derivations for the declarative type system of Figure 4 can still take many different shapes. In this section, we define several normalisation lemmas, each restricting the use of a non-structural rule. They are then combined into a normalisation theorem.

**Normalisation of `[v]` nodes**

**LEMMA I.5 (INTRODUCTION OF AN ARBITRARY `[v]` NODE).** Let Γ a type environment, *e* and *e*<sub>x</sub> two expressions, and `{u<sub>i</sub>}`<sub>i∈I</sub> a partition of 1. Let *D* be a derivation for the judgement Γ+e{e<sub>x</sub>/x} : t such that *D* does not contain any `[v]` node performing a substitution {e<sub>y</sub>/y} with e<sub>y</sub> a strict sub-expression of e<sub>x</sub>. If e<sub>x</sub> is typable under the context Γ, then there exists a type s such that *D* can be transformed into a derivation whose root is a `[v]` node of the following form:

$$ [v] \frac{\frac{\dots}{\Gamma \vdash e_x : s} \quad \frac{\dots}{\Gamma, x : s \wedge u_i \vdash e : t} \quad \forall i \in I}}{\Gamma \vdash e \{e_x/x\} : t} $$

**PROOF.** Let *C* a derivation for Γ+e<sub>x</sub> : 1. We collect in *D* the set {*C*<sub>*k*</sub>}<sub>*k*∈*K*</sub> of all the subderivations for the expression e<sub>x</sub>. As substitutions are capture-avoiding, no variable in fv(e<sub>x</sub>) could have been introduced in the environment by a `[→I]` or `[v]` node in *D*. Thus, we know that the derivations {*C*<sub>*k*</sub>}<sub>*k*∈*K*</sub> are still valid under the initial environment Γ.

Thus, we can build the following derivation:

$$ [v] \frac{\frac{\frac{C}{\Gamma \vdash e_x : 1} \quad \frac{C_k}{\Gamma \vdash e_x : t_k}}{\Gamma \vdash e_x : \Lambda_{k \in K} t_k}}{\Gamma, x : (\Lambda_{k \in K} t_k) \wedge u_i \vdash e : t} \quad \forall i \in I} \quad \Gamma \vdash e \{e_x/x\} : t $$

with each $D'_i$ being a derivation easily derived from *D* by substituting $e_x$ by *x* when relevant, using a `[Ax_ν]` rule on *x* instead of a subderivation for $e_x$ when necessary, and by using monotonicity (Lemma I.4). The hypothesis on the derivation *D* ensures that it does not contain any conflicting `[v]` node that would become inapplicable due to the fact that $e_x$ has been substituted by *x*. □

**LEMMA I.6 (ELIMINATION OF ALIASING).** Let *D* be a ground derivation, and *N* be a `[v]` node in *D* applying a substitution {x/y}. Then, *N* can be removed from *D*, without adding any new `[v]` node nor structural node in *D*.

**PROOF.** The following transformation can be performed to the subderivation introducing *x* (as *D* is a ground derivation, there must be a `[v]` node that introduces *x*):
$$ [\mathbf{V}] \frac{\frac{A}{\Gamma \vdash e_x : s} \quad \frac{B}{\Gamma, x : s \wedge \mathbf{u}_k \vdash e : t} \quad \frac{E_i}{\Gamma, x : s \wedge \mathbf{u}_i \vdash e : t} \quad \forall i \in I \setminus \{k\}}{\Gamma \vdash e\{e_x/x\} : t} $$

where B is a derivation that contains this subderivation S

(whose root is the node N to eliminate):

$$ [\mathbf{V}] \frac{\frac{C}{\Gamma' \vdash x : s'} \quad \frac{D_j}{\Gamma', y : s' \wedge \mathbf{u}'_j \vdash e' : t'} \quad \forall j \in J}{}{\Gamma' \vdash e'\{x/y\} : t'} $$

with $\Gamma' = (\Gamma, x : s \wedge \mathbf{u}_k) \cup \Gamma''$ for some $\Gamma''$

↓ (transformed into)

$$ [\mathbf{V}] \frac{\frac{A}{\Gamma \vdash e_x : s} \quad \frac{B'_j}{\Gamma, x : s \wedge \mathbf{u}_k \wedge \mathbf{u}'_j \vdash e : t} \quad \forall j \in J}{}{\Gamma \vdash e\{e_x/x\} : t} \quad \forall i \in I \setminus \{k\} $$

where $B'_j$ is constructed from B by monotonicity (Lemma I.4),

and by replacing the subderivation S by this one:

$$ \frac{D'_j}{(\Gamma, x : s \wedge \mathbf{u}_k \wedge \mathbf{u}'_j) \cup \Gamma'' \vdash e'\{x/y\} : t'} $$

where $D'_j$ is constructed from $D_j\{x/y\}$ by monotonicity (Lemma I.4) (★)

(★) Note that we have $s \wedge \mathbf{u}_k \le_P s'$ as the only structural rule that the derivation C can use is $[Ax_\vee]$ on x, and thus $s \wedge \mathbf{u}_k \wedge \mathbf{u}'_j \le s' \wedge \mathbf{u}'_j$. □

An interesting thing to note is that the proof above would not work in the presence of a generalization rule such as the one used at top-level:

$$ [\text{GEN}] \frac{\Gamma \vdash e : t}{\Gamma \vdash e : t \phi} \phi \# \Gamma $$

Indeed, the guard condition $\phi \# \Gamma$ may prevent monotonicity. More precisely, in the transformation above, if the partition $\{\mathbf{u}_i\}_{i \in I}$ introduces a new monomorphic type variable, its introduction earlier in the environment might prevent a potential application of a [GEN] rule in the derivation B. This impossibility to eliminate aliasing would be an issue for the normalisation lemma (Lemma I.13) detailed below, as it states, in particular, that the union elimination rule only needs to be applied once for a given sub-expression. This is the reason why, in our declarative type system, generalisation only occurs at top-level.

**DEFINITION I.7 (ACCEPTABLE [V] NODE).** In any derivation, a [V] node N doing the substitution $e\{e'/x\}$ is said acceptable if it satisfies the following constraints:

* e contains x (no useless definition), and

* e does not contain e' (maximal sharing), and
* *e'* is not a binding variable (no aliasing)

**DEFINITION I.8 (BINDING CONTEXT).** A binding context $B$ is an ordered list of mappings from binding variables to atoms. Each mapping is written as a pair $(x, e)$. We note these lists extensionally by separating elements by a semicolon, that is, $(x_1, a_1); \dots; (x_n, a_n)$ and use $\epsilon$ to denote the empty list. We note $eB$ the expression $e\{e_n/x_n\} \dots \{e_1/x_1\}$ where $(x_1, e_1); \dots; (x_n, e_n)$ are the pairs in $B$.

Given a derivation $D$ and a node $N$ of $D$, we call binding context of $N$ in $D$ the binding context $(x_1, e_1); \dots; (x_n, e_n)$, where $\{e_1/x_1\}; \dots; \{e_n/x_n\}$ are the substitutions made by all the $[\vee]$ nodes crossed by one of their body premises when going from the root of $D$ to $N$.

In the following definition, we use an order over expressions:

**DEFINITION I.9 (EXPRESSION ORDER).** A (possibly partial) order $\leq$ is called expression order if it is an order over expressions modulo $\alpha$-renaming, and if it is an extension of the sub-expression order: if $e_1$ is a sub-expression of $e_2$ modulo $\alpha$-renaming, then we should have $e_1 \leq e_2$. We write $e_1 < e_2$ when $e_1 \leq e_2$ and $e_2 \not\leq e_1$.

**DEFINITION I.10 (WELL-POSITIONNED [V] NODE).** A $[\vee]$ node $N$ of a derivation $D$, of binding context $B$ in $D$ and doing the substitution $e\{e_1/x\}$, is said well-positionned in $D$ relatively to the expression order $\leq$ (or more succintly, well-positionned in $(D, \leq)$) if there is no node $N'$ on the path from the root to $N$ such that:

* Every variable in $fv(e_1B)$ is in the type environment of $N'$, and

* $N'$ is not a $[\vee]$ rule, or $N'$ is a $[\vee]$ rule of binding context $B'$ and performing a substitution $\{e_2/\gamma\}$ such that $e_1B < e_2B'$.

**DEFINITION I.11 ([V]-CANONICAL DERIVATION).** For a given expression order $\leq$, a derivation $D$ is $[\vee]$-canonical for the order $\leq$ if every $[\vee]$ node it contains is acceptable and well-positionned in $(D, \leq)$.

**DEFINITION I.12 (FORM DERIVATIONS, ATOMIC DERIVATIONS).** A derivation $D$ is a form derivation if every segment of branch containing the root and stopping at the first $[\vee]$ node (if any, or stopping at a leaf otherwise):

* does not contain any structural node, and

* if it ends with a $[\vee]$ node $N$, the definition premise of $N$ is an atomic derivation, and the body premises of $N$ are form derivations.

A derivation $D$ is an atomic derivation if every segment of branch containing the root and stopping at the first $[\rightarrow I]$ node (if any, or stopping at a leaf otherwise):

* does not contain any $[\vee]$ node, and

* contains exactly one structural node, and

* if it ends with a $[\rightarrow I]$ node $N$, the premise of $N$ is a form derivation.

A derivation that is both a $[\vee]$-canonical derivation and a form derivation is called $[\vee]$-canonical form derivation.

**LEMMA I.13 (NORMALISATION OF [V]).** Given an expression order $\leq$, any ground derivation $D$ of $\Gamma \vdash e : t$ can be transformed into a $[\vee]$-canonical form derivation of $\Gamma \vdash e : t'$ for the order $\leq$ and with $t' \leq_P t$.

**PROOF.** First, we can remove any aliasing (i.e. $[\vee]$ nodes doing a substitution $\{y/x\}$) by applying Lemma I.6 as needed. We can also trivially remove useless $[\vee]$ nodes (i.e. those doing a substitution $e\{e_x/x\}$ where $e$ does not contain $x$).

Then, let's consider, in the whole derivation, all the nodes that satisfy one of those conditions:
* It is a structural node *N* such that, when going towards the root, it crosses another structural node before crossing a [→I] node.

* It is a structural node *N* such that, when going towards the root, it crosses a [∀] node by one of its body premises before crossing a [∀] node by its definition premise.

* It is a [∀] node that is not acceptable or not well-positionned in (D, ≤).

If there is no such node, then the properties of Lemma I.13 are satisfied. Otherwise, we associate to each of these faulty nodes an expression and a binding context:

* For a structural node applied on an expression *e* in a binding context *B*, we associate (*e*, *B*),

* For a [∀] node doing the substitution {$e_x/x$} in a binding context *B*, we associate ($e_x$, *B*).

Now, we select among those nodes the one whose associated pair is minimal with respects to the following order: ($e_1$, $B_1$) is smaller than ($e_2$, $B_2$) if and only if $e_1B_1 \le e_2B_2$. Let's call this node *N*, and its associated expression and binding context *e* and *B* respectively.

Now, let's locate, in the segment from the root to *N*, the farthest location *L* from the root such that *N* would be well-positionned in (*D*, ≤) at this location.

Let's note $\Gamma_L \vdash e_L : t_L$ the judgement at this location. We consider the subderivation $D_L$ that derives this judgement in *D*. Note that, in $D_L$, there is no [∀] node that makes a substitution {$e_\gamma/\gamma$} with $e_\gamma$ a strict sub-expression of *e*, because $e_\gamma B_\gamma$ (with $B_\gamma$ the binding context of the corresponding [∀] node) would be smaller than $eB$ for ≤, thus making it not well-positionned and contradicting the minimality of ($e$, $B$). Also note that $D_L$ contains the node *N* (otherwise, the [∀] node *N* would not be well-positionned at location *L*).

We apply Lemma I.5 on the root of $D_L$ so that it performs the substitution $e'_L\{e/z\}$ using the decomposition $\{\mathbf{u}_i\}_{i \in I} = \{\mathbf{1}\}$, with z fresh and $e'_L$ an expression that does not contain *e* and such that $e'_L\{e/z\} \equiv e_L\{e/z\}$ (basically, $e'_L$ is $e_L$ where occurrences of *e* have been replaced by *z*). This lemma can be applied as:

* There cannot be in our subderivation any [∀] node substituting a strict sub-expression of *e*,

* We know that $\Gamma_L \vdash e : \mathbf{1}$ holds: we can derive it from the definition premise of *N* if *N* is a [∀] node, or from *N* itself if *N* is a structural node.

This gives us a new derivation $D'_L$.

If *N* is a [∀] node, *N* can be removed in $D'_L$ by using Lemma I.6, as well as other aliasing that would have been introduced in other branches. Not that, if *N* is a structural node, it has already been eliminated by the application of Lemma I.5. Finally, we replace the subderivation $D_L$ by $D'_L$ in *D*.

We conclude by repeating this whole process until all the nodes satisfy the conditions. We are guaranteed that it terminates by the fact that $eB$ strictly increases for $\le$ at each iteration (with ($e$, $B$) the pair associated to the choosen node *N*). $\square$

**Normalisation of [Inst] nodes**

**LEMMA I.14.** *A derivation Γ ⊢ e : t can be transformed into a derivation Γ ⊢ e : tρ (for any renaming ρ) without changing the structure of the derivation).*

**PROOF.** Any polymorphic type variable in *t* must be introduced either by a [Ax_λ], [Ax_∀], or [Inst] rule. Thus, we can derive Γ ⊢ e : tρ by induction on Γ ⊢ e : t, where:

* Every renaming $\rho'$ of a [Ax_λ] or [Ax_∀] node is replaced by the renaming $\rho \circ \rho'$, and

* Every substitution $\sigma$ of a [Inst] node is replaced by the substitution $\rho \circ \sigma \circ \rho^{-1}$.

$\square$

**PROPOSITION I.15.** *If $\forall i \in I$. $t'_i \leq_P t_i$, then $\bigwedge_{i \in I} t'_i \leq_P \bigwedge_{i \in I} t_i.$
PROOF. For each $i \in I$, let $\Sigma_i$ a set of substitutions such that $t'_i \Sigma_i \le t_i$. We consider the set of substitutions $\Sigma = \bigcup_{i \in I} \Sigma_i$, and we show that $(\bigwedge_{i \in I} t'_i) \Sigma \le \bigwedge_{i \in I} t_i$.

We have:

$$ \begin{align*} \bigwedge_{\sigma \in \Sigma} (\bigwedge_{i \in I} t'_i) \sigma &\approx \bigwedge_{i \in I} \bigwedge_{\sigma \in \Sigma_i} (\bigwedge_{j \in I} t'_j) \sigma \\ &\le \bigwedge_{i \in I} \bigwedge_{\sigma \in \Sigma_i} t'_i \sigma \\ &\le \bigwedge_{i \in I} t_i \end{align*} $$

□

PROPOSITION I.16. If $\forall i \in I$. $t'_i \le_P t_i$ and all $\{t_i\}_{i \in I}$ have disjoint polymorphic type variables, then
$\bigvee_{i \in I} t'_i \le_P \bigvee_{i \in I} t_i$.

PROOF. For each $i \in I$, let $\Sigma_i$ a set of substitutions such that $t'_i \Sigma_i \le t_i$. We consider the set of substitutions $\Sigma = \{\sigma_1 \dot{\cup} \dots \dot{\cup} \sigma_n \mid \sigma_1 \in \Sigma_1, \dots, \sigma_n \in \Sigma_n\}$ for $I = \{1, \dots, n\}$, where $\dot{\cup}$ denotes the composition of disjoint substitutions (their disjointness is guaranteed by the fact that all $\{t'_i\}_{i \in I}$ have disjoint polymorphic type variables), and we show that $(\bigvee_{i \in I} t'_i) \Sigma \le \bigvee_{i \in I} t_i$.

We have:

$$ \begin{align*} \bigwedge_{\sigma \in \Sigma} (\bigvee_{i \in 1..n} t'_i) \sigma & \\ &\approx \bigwedge_{(\sigma_1, \dots, \sigma_n) \in \Sigma_1 \times \dots \times \Sigma_n} (\bigvee_{i \in 1..n} t'_i)(\sigma_1 \dot{\cup} \dots \dot{\cup} \sigma_n) \\ &\approx \bigwedge_{(\sigma_1, \dots, \sigma_n) \in \Sigma_1 \times \dots \times \Sigma_n} \bigvee_{i \in 1..n} t'_i(\sigma_1 \dot{\cup} \dots \dot{\cup} \sigma_n) \\ &\approx \bigwedge_{(\sigma_1, \dots, \sigma_n) \in \Sigma_1 \times \dots \times \Sigma_n} \bigvee_{i \in 1..n} t'_i \sigma_i \\ &\approx \bigvee_{i \in 1..n} \bigwedge_{\sigma_i \in \Sigma_i} t'_i \sigma_i \tag{distributivity of $\vee$ over $\wedge$} \\ &\le \bigvee_{i \in 1..n} t_i \end{align*} $$

□

DEFINITION I.17 (
-CANONICAL DERIVATION). A derivation $D$ is 
-canonical if every

 node it contains is part of a [INST$\wedge\le$] pattern that is either:

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

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

* One of the premises of a $[\rightarrow E]$ node

LEMMA I.18 (NORMALISATION OF 
). Given an expression order $\le$, any $[\vee]$-canonical form
derivation $D$ of $\Gamma \vdash e : t$ can be transformed into a $[\vee][\text{INST}]-$canonical form derivation of $\Gamma \vdash e : t'$ for
the order $\le$ and with $t' \le_P t$.

PROOF. We proceed by induction on $(n_\vee, n)$ (using the lexicographic order), where $n_\vee$ denotes the
number of $[\vee]$ nodes in the derivation, and $n$ denotes the total number of nodes in the derivation.

If the root is a 
 or $[\le]$, we can remove the root (its premise will be the new root) and
proceed inductively on the result.

If the root is a $[\wedge]$, we proceed inductively on all its premises and update the intersection type $t$
derived by the root into a new intersection type $t'$ (according to the new premises). We know that
the new derived type $t'$ satisfies $t' \le_P t$ according to Proposition I.15.

If the root is a $[\vee]$ of the following form:

$$ [\vee] \frac{\frac{A}{\Gamma \vdash e' : s} \quad \frac{B_i}{\Gamma, x : s \wedge \mathbf{u}_i \vdash e : t} \quad \forall i \in I} {\Gamma \vdash e\{e'/x\} : t} $$
(1) We first proceed inductively on A, which gives a derivation A'. We consider following derivation, where $s' \le_P s$ (and thus $s' \wedge \mathbf{u}_i \le_P s \wedge \mathbf{u}_i$):

$$ [\vrule] \frac{\frac{A'}{\Gamma \vdash e' : s'} \qquad \frac{B'_i}{\Gamma, x : s' \wedge \mathbf{u}_i \vdash e : t} \qquad \forall i \in I} {\Gamma \vdash e\{e' / x\} : t} $$

with $B'_i$ a derivation easily derived from $B_i$ by monotonicity (Lemma I.4). Note that the application of the monotonicity lemma might insert unwanted $[\text{Inst} \wedge \le]$ patterns after axioms, but they will be eliminated with the next step.

(2) The next step is to proceed inductively on the $\{B'_i\}_{i \in I}$ premises, yielding some derivations $\{B''_i\}_{i \in I}$ that derive some types $\{t_i\}_{i \in I}$ (with $\forall i \in I. t_i \le_P t$). We can suppose that all the $\{t_i\}_{i \in I}$ have disjoint polymorphic type variables: if it is not the case, it can be ensured by applying Lemma I.14 to these premises. Then, we consider the following derivation:

$$ [\vrule] \frac{\frac{A'}{\Gamma \vdash e' : s'} \qquad \frac{B''_i}{[\le] \frac{\Gamma, x : s' \wedge \mathbf{u}_i \vdash e : t_i}{\Gamma, x : s' \wedge \mathbf{u}_i \vdash e : \bigvee_{i \in I} t_i}} \qquad \forall i \in I} {\Gamma \vdash e\{e' / x\} : \bigvee_{i \in I} t_i} $$

The result $\bigvee_{i \in I} t_i$ satisfies $\bigvee_{i \in I} t_i \le_P t$ according to Proposition I.16.

(3) The new $[\le]$ nodes that appear as premise of the $[\vrule]$ root could break the properties of Lemma I.13 if the corresponding $B''_i$ ends with a $[\vrule]$ node. In this case, we move up the faulty $[\le]$ nodes as needed using this transformation:

$$ [\vrule] \frac{\frac{A}{\Gamma \vdash e' : s} \qquad \frac{B_i}{\Gamma, x : s \wedge \mathbf{u}_i \vdash e : t'} \qquad \forall i \in I} {\Gamma \vdash e\{e' / x\} : t'} $$

↓

$$ [\vrule] \frac{\frac{A}{\Gamma \vdash e' : s} \qquad \frac{B_i}{[\le] \frac{\Gamma, x : s \wedge \mathbf{u}_i \vdash e : t'}{\Gamma, x : s \wedge \mathbf{u}_i \vdash e : t}} \qquad \forall i \in I} {\Gamma \vdash e\{e' / x\} : t} $$

The other cases are straightforward. □

### Normalisation of $[\le]$ nodes

**DEFINITION I.19** ($[\le]$-CANONICAL DERIVATION). A derivation $D$ is $[\le]$-canonical if every $[\le]$ node it contains is either:

* The first premise of a $[\in_1]$ or $[\in_2]$ node, or

* One of the body premises of a $[\vrule]$ node, or

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

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

**LEMMA I.20** (NORMALISATION OF $[\le]$). Given an expression order $\le$, any $[\vrule][\text{Inst}]$-canonical form derivation $D$ of $\Gamma \vdash e : t$ can be transformed into a $[\vrule][\text{Inst}][\le]$-canonical form derivation of $\Gamma \vdash e : t'$ for the order $\le$ and with $t' \le_P t$.
PROOF. We proceed by induction on $(n_\vee, n)$ (using the lexicographic order), with $n_\vee$ the number of $[\vee]$ nodes in the derivation, and $n$ the total number of nodes in the derivation.

If the root is a $[\le]$ or $[\text{Inst}]$, we can remove the root (its premise will be the new root) and proceed by induction on its premise.

If the root is a $[\wedge]$, we proceed inductively on all its premises and update the intersection type $t$ derived by the root into a new intersection type $t'$ (according to the new premises). We trivially have $t' \le_p t$.

If the root is a $[\rightarrow I]$ pattern, we proceed inductively on its premise and update the arrow type $t$ derived by the root into a new arrow type $t'$ (according to the new premise). We trivially have $t' \le_p t$.

If the root is a $[\vee]$ of the following form:

$$ [\vee] \frac{\frac{A}{\Gamma \vdash e' : s} \qquad \frac{B_i}{\Gamma, x : s \wedge \mathbf{u}_i \vdash e : t} \quad \forall i \in I} {\Gamma \vdash e\{e' / x\} : t} $$

(1) We first proceed inductively on $A$, yielding a derivation $A'$. We then consider the following derivation, with $s' \le_p s$:

$$ [\vee] \frac{\frac{A'}{\Gamma \vdash e' : s'} \qquad \frac{B'_i}{\Gamma, x : s' \wedge \mathbf{u}_i \vdash e : t} \quad \forall i \in I}}{\Gamma \vdash e\{e' / x\} : t} $$

where each $B'_i$ is derived from $B_i$ by applying Lemma I.4 (monotonicity), and then Lemma I.18 in order to normalize $[\text{Inst}]$ nodes that might have been introduced by the monotonicity lemma. Note that this might add unwanted $[\le]$ nodes, but they will be eliminated with the next step.

(2) We proceed inductively on the $\{B'_i\}_{i \in I}$ premises, yielding some derivations $\{B''_i\}_{i \in I}$ that derive some types $\{t_i\}_{i \in I}$ (with $\forall i \in I$. $t_i \le_p t$). Then, we consider the following derivation:

$$ [\vee] \frac{\frac{A'}{\Gamma \vdash e' : s'} \qquad \frac{B''_i}{\Gamma, x : s' \wedge \mathbf{u}_i \vdash e : t_i} \quad \forall i \in I} {\Gamma, x : s' \wedge \mathbf{u}_i \vdash e : \bigvee_{i \in I} t_i} \qquad \forall i \in I $$

The result $\bigvee_{i \in I} t_i$ trivially satisfies $\bigvee_{i \in I} t_i \le_p t$.

(3) The new $[\le]$ nodes that appear as premise of the $[\vee]$ root could break the properties of Lemma I.13 if the corresponding $B''_i$ ends with a $[\vee]$ node. In this case, we move up the
faulty [≤] nodes as needed using this transformation:

$$ \frac{\frac{A}{\Gamma \vdash e' : s} \qquad \frac{B_i}{\Gamma, x : s \wedge \mathbf{u}_i \vdash e : t'} \quad \forall i \in I} {\boxed{\phantom{A}} \qquad \boxed{\phantom{B_i}} \qquad \forall i \in I} } {\boxed{\phantom{A}} \qquad \boxed{\phantom{B_i}} \qquad \forall i \in I} } $$

↓

$$ \frac{\frac{A}{\Gamma \vdash e' : s} \quad [\le] \quad \frac{B_i}{\Gamma, x : s \wedge \mathbf{u}_i \vdash e : t'} \quad \forall i \in I} {\boxed{\phantom{A}} \qquad \boxed{\phantom{B_i}} \qquad \forall i \in I} } {\boxed{\phantom{A}} \qquad \boxed{\phantom{B_i}} \qquad \forall i \in I} } $$

The other cases are straightforward. □

**DEFINITION I.21 (CANONICAL DERIVATION).** Given an expression order $≤$, a canonical derivation for the expression order $≤$ is a $[\lor][\text{Inst}][\le]$-canonical derivation. We say it is a canonical form derivation if it is also a form derivation, and a canonical atomic derivation if it is an atomic derivation.

When qualifying a derivation $D$ of canonical, the order $≤$ may be omitted: in this case, we consider that there exists an expression order $≤$ such that $D$ is canonical for $≤$.

**THEOREM I.22 (NORMALISATION OF DERIVATIONS).** Given an expression order $≤$, any ground derivation $D$ of $Γ \vdash e : t$ can be transformed into a canonical form derivation of $Γ \vdash e : t'$, for the order $≤$ and with $t' ≤_P t$.

**PROOF.** By successive application of Lemma I.13, Lemma I.18, and Lemma I.20. □

## I.2 Type Safety

I.2.1 *The Parallel Semantics.* One technical difficulty is that the subject reduction does not hold for the semantics presented in Figure 1: performing a reduction step on an expression *e* might break the use of a [*v*] rule. Indeed, if in the original typing derivation a rule [*v*] substitutes multiple occurrences of the sub-expression *e* by a variable *x*, reducing one occurrence of *e* but not the others can make the application of this [*v*] rule impossible: the correlation between the reduced *e* and the other occurrences of *e* is thus 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 first define reduction rules that only apply at top-level, and then define a context rule (rule [*κ*] below) that allows reducing under an evaluation context, but that will apply this reduction everywhere in the term. With this alternative semantics, the subject reduction becomes true, allowing to prove type safety. The type safety for the initial semantics (Figure 1) is then deduced from this result.

The parallel semantics is formalized in Figure 5. A step of reduction happening at top-level is noted $\to_T$, and a step of reduction of the parallel semantics under any evaluation context is noted $\to_P$. Notice that the rule [*κ*] applies on an expression $e''$ a substitution from an expression $e'$ to an expression $e$, noted $e''\{e/e'\}$, which is defined inductively on $e''$ 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
**Top-level reductions:**

$$ (\lambda x.e)v \underset{\to}{\to}_{\tau} e\{v/x\} \qquad (7) $$

$$ \pi_1(v_1, v_2) \underset{\to}{\to}_{\tau} v_1 \qquad (8) $$

$$ \pi_2(v_1, v_2) \underset{\to}{\to}_{\tau} v_2 \qquad (9) $$

$$ (v \in \tau) ? e_1 : e_2 \underset{\to}{\to}_{\tau} e_1 \quad \text{if } v \in \tau \qquad (10) $$

$$ (v \in \tau) ? e_1 : e_2 \underset{\to}{\to}_{\tau} e_2 \quad \text{if } v \in \neg \tau \qquad (11) $$

**Parallel reductions:**

$$ [\kappa] \frac{e \underset{\to}{\to} e'}{E[e] \underset{\to}{\to} \varphi (E[e])\{e'/e\}} $$

**Evaluation Context** $E ::= [] | vE | Ee | (v, E) | (E, e) | (E \in \tau) ? e : e$

<caption>Fig. 5. Parallel Semantics</caption>

$$
\begin{align*}
c\{e/e'\} &= c \\
x\{e/e'\} &= x \\
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 \mathrm{fv}(e') \\
(\lambda x.e_0)\{e/e'\} &= \lambda x.(e_0\{e/e'\}) \qquad x \notin \mathrm{fv}(e) \cup \mathrm{fv}(e') \\
(\lambda x.e_0)\{e/e'\} &= \lambda y.((e_0\{y/x\})\{e/e'\}) \qquad x \notin \mathrm{fv}(e), x \in \mathrm{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'\}
\end{align*}
$$

In particular, notice that expression substitutions are up to $\alpha$-renaming and perform only one pass. Here is an example of reduction step using the parallel semantics:

$$ [\kappa] \frac{(\lambda x.x)(\lambda x.x) \underset{\to}{\to} \lambda x.x}{((\lambda x.x)(\lambda x.x), (\lambda x.x)(\lambda x.x)) \underset{\to}{\to} \varphi (\lambda x.x, \lambda x.x)} $$

### 1.2.2 Subject Reduction.

**PROPOSITION I.23.** If $\Gamma \vdash v : \tau$, then $v \in \tau$ (see Figure 1 for the definition of $\in$).

**PROOF.** Straightforward, by induction on the derivation of the judgement $\Gamma \vdash v : \tau$. Note that the case of $\lambda$-abstractions is trivial as arrows in $\tau$ can only be $\emptyset \to 1$. $\square$

**LEMMA I.24 (SUBSTITUTION LEMMA).** If $\Gamma, x : s \vdash e : t$ and $\Gamma \vdash e' : s$, then $\Gamma \vdash e\{e'/x\} : t$.

**PROOF.** Straightforward induction on the derivation $\Gamma, x : s \vdash e : t$, where each $[\mathrm{Ax}_\lambda]$ node is replaced by the derivation $\Gamma \vdash e' : s$. $\square$

**DEFINITION I.25 (ATOMIC TYPE).** A type $t$ is said atomic if it cannot be decomposed into a non-trivial union. Formally, $t$ is atomic if and only if, for any set of types $\{t_i\}_{i \in I}$, $t \le \bigvee_{i \in I} t_i \Rightarrow \exists i \in I. t \le t_i$. Equivalently, $t$ is atomic if and only if, for any type $s$, either $t \le s$ or $t \le \neg s$.
**LEMMA I.26 (ATOMICITY OF VALUE TYPES).** If there exists a canonical atomic derivation $D$ of $\Gamma \vdash \nu : s$ (with $\nu$ a value), then $s$ is atomic.

**PROOF.** As $\nu$ is a value, we know that the derivation does not contain any destructor nor axiom node, except possibly in the premise of a $[\rightarrow I]$ node. Moreover, as $D$ is a canonical atomic derivation, it does not contain any $[\vee]$ nor $[\le]$ node neither. In particular, this implies that $s$ cannot contain any type variable nor union, except under an arrow. More precisely, we can easily prove that $s$ can be constructed with the following syntax:

$$ \textbf{Value Type} \quad \bar{t} ::= b \mid t \rightarrow t \mid \bar{t} \times \bar{t} \mid \bar{t} \land \bar{t} $$

Any type $t_1 \rightarrow t_2$ is atomic, so is any base type $b$. Atomicity is preserved by intersection and product, thus we can deduce that a type constructed with the syntax above is atomic. $\square$

**DEFINITION I.27 (UNAVOIDABLE $[\vee]$ NODE).** In any derivation, a $[\vee]$ node $N$ doing the substitution $e\{e'/x\}$ is said unavoidable if $N$ is acceptable (Definition I.7) and if $e'$ is not a value. A $[\vee]$ node that is not unavoidable is said avoidable.

**DEFINITION I.28 (MINIMAL DERIVATION).** A derivation is said minimal if every $[\vee]$ node it contains is unavoidable.

**LEMMA I.29 (ELIMINATION OF VALUE SUBSTITUTIONS).** Any canonical form derivation or canonical atomic derivation $D$ of $\Gamma \vdash e : t$ can be transformed into a minimal derivation of $\Gamma \vdash e : t$.

**PROOF.** We proceed by structural induction on $D$.

If the root is not a $[\vee]$ node, or if it is an unavoidable $[\vee]$ node, then we proceed inductively on all its premises.

Otherwise, if the root is an avoidable $[\vee]$ node, we know that it is doing a substitution $e\{v/x\}$ with $v$ a value (as $D$ is canonical, the $[\vee]$ node must be acceptable). We can thus apply Lemma I.26 on its definition premise $\Gamma \vdash \nu : s$; we deduce that $s$ is atomic. Consequently, among the types $\{u_i\}_{i \in I}$ composing the partition of $1$ used by this node, there is a type $u_i$, for some $i \in I$, such that $s \le u_i$.

We consider the corresponding body premise $\Gamma, x : s \vdash e : t$, and we proceed by induction on it in order to get a minimal derivation $D'$ for $\Gamma, x : s \vdash e : t$. Similarly, we proceed by induction on the definition premise $\Gamma \vdash \nu : s$ in order to get a minimal derivation $A$ for $\Gamma \vdash \nu : s$.

We can then derive $\Gamma \vdash e\{v/x\} : t$ from $D'$ by replacing $[Ax_\vee]$ nodes applying on $x$ by the derivation $A$ (in a similar way as done in Lemma I.24, but for a binding variable). This new derivation is minimal. $\square$

**LEMMA I.30 (SUBJECT REDUCTION).** If $D$ is a minimal derivation for $\Gamma \vdash e : t$, and if $e_o \rightarrow \tau e'_o$, then $\Gamma \vdash e'_{o}/e_o : t$.

**PROOF.** We proceed by structural induction on $D$.

If $e$ contains no occurrence of $e_o$ (modulo $\alpha$-renaming), this result is trivial. Thus, we will suppose in the following that $e$ contains at least one occurrence of $e_o$.

We denote by $e'$ the expression $e'_{o}/e_o$, and consider the root of the derivation:

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

[Ax_\lambda] Impossible case ($e$ cannot contain any reducible expression).

[Ax_\vee] Impossible case ($e$ cannot contain any reducible expression).

$[\le]$ 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 a $[\le]$ node.


 Similar to the previous case.
[∧] We proceed inductively on each premise, and intersect the resulting derivations with a [∧] node.

[→I] We have $e' \equiv \lambda x. (e_\lambda\{e'_o/e_o\})$ for some expression $e_\lambda$. We can derive $\Gamma, x : \mathbf{u} \dashv e_\lambda\{e'_o/e_o\} : t'$ by induction on the premise $\Gamma, x : \mathbf{u} \dashv e_\lambda : t'$ (with $t \approx \mathbf{u} \to t'$) and conclude by using a [→I] node.

[×I] We have $e' \equiv (e_1\{e'_o/e_o\}, e_2\{e'_o/e_o\})$ for some $e_1$ and $e_2$. We proceed inductively on the premises, as in the previous case.

[→E] We have $e \equiv e_1 e_2$ for some expressions $e_1$ and $e_2$. If $e_o$ is a sub-expression of $e_1$ and/or $e_2$, we conclude by proceeding inductively on the premises, as in the previous case.

Otherwise, $e_o \equiv e_1 e_2$ and thus the reduction $e_o \rightsquigarrow e'_o$ uses the rule 7. Consequently, we know that $e_o \equiv e \equiv (\lambda x. e_\lambda)v$ for some expression $e_\lambda$ and value $v$, and $e'_o \equiv e' \equiv e_\lambda\{v/x\}$.

We have the following premises:

(1) $\Gamma \dashv \lambda x. e_\lambda : t_1 \to t_2$ (with $t_2 \approx t$)

(2) $\Gamma \dashv v : t_1$

As D is minimal, we know that the premise (1) has no [⊤] node, except possibly in the premise of a [→I] node. Thus, we can extract from (1) a collection of derivations of the judgements $\Gamma, x : \mathbf{u}_i \dashv e_\lambda : s_i$ for $i \in I$, such that there exists some instantiations $\Sigma_i$ such that $\bigwedge_{i \in I}(\mathbf{u}_i \to s_i)\Sigma_i \le t_1 \to t_2$. We have $\bigwedge_{i \in I}\mathbf{u}_i \to s_i\Sigma_i \approx \bigwedge_{i \in I}(\mathbf{u}_i \to s_i)\Sigma_i \le t_1 \to t_2$. Moreover, using [INST∧≤] patterns, we can derive for each $i \in I$ the judgement $\Gamma, x : \mathbf{u}_i \dashv e_\lambda : s_i\Sigma_i$.

Now, let's consider a partition $\{\mathbf{v}_j\}_{j \in J}$ of $\bigvee_{i \in I} \mathbf{u}_i$ of minimal cardinality such that: $\forall j \in J. \forall i \in I. \mathbf{v}_j \le \mathbf{u}_i$ or $\mathbf{v}_j \wedge \mathbf{u}_i \approx \emptyset$. We know that $J$ is not empty: the case $t_1 \le \bigvee_{i \in I} \mathbf{u}_i \approx \emptyset$ is impossible since the value $v$ would have type $\emptyset$, contradicting Proposition I.23. For every $j \in J$, we define $I_j = \{i \in I | \mathbf{v}_i \wedge \mathbf{u}_i \ne \emptyset\}$ ($I_j$ cannot be empty as the partition $\{\mathbf{v}_j\}_{j \in J}$ has minimal cardinality). Note that for any $j \in J$ and $i \in I_j$, we have $\mathbf{v}_j \le \mathbf{u}_i$.

Using the monotonicity lemma (Lemma I.4), we can derive for every $j \in J$ and $i \in I_j$ the judgement $\Gamma, x : \mathbf{v}_j \dashv e_\lambda : s_i\Sigma_i$. Thus, using a [∧] node, for every $j \in J$ we can derive $\Gamma, x : \mathbf{v}_j \dashv e_\lambda : \bigwedge_{i \in I_j} s_i\Sigma_i$. Moreover, as $\bigwedge_{i \in I_j} \mathbf{u}_i \to s_i\Sigma_i \le t_1 \to t_2$, we have, for every $j \in J$, $\bigwedge_{i \in I_j} s_i\Sigma_i \le t_2$. Consequently, for every $j \in J$, we can derive the judgement $\Gamma, x : \mathbf{v}_j \dashv e_\lambda : t_2$ using a [≤] node. Combining these judgements with a [⊤] node allows us to derive $\Gamma, x : \bigvee_{j \in J} \mathbf{v}_j \dashv e_\lambda : t_2$.

As $\bigvee_{j \in J} \mathbf{v}_j$ covers $t_1$, we can construct from (2) a derivation $\Gamma \dashv v : \bigvee_{j \in J} \mathbf{v}_j$ using a [≤] node. Finally, applying the substitution lemma (Lemma I.24) gives a derivation for $\Gamma \dashv e_\lambda\{v/x\} : t_2$.

[×E1] We have $e \equiv \pi_1 e_1$ for some expression $e_1$. If $e_o$ is a sub-expression of $e_1$, we conclude by proceeding inductively on the premise.

Otherwise, $e_o \equiv \pi_1 e_1$ and thus the reduction $e_o \rightsquigarrow e'_o$ uses the rule 8. Consequently, we know that $e_o \equiv e \equiv \pi_1(v_1, v_2)$ for some values $v_1$ and $v_2$, and $e'_o \equiv e' \equiv v_1$.

Similarly to the previous case, as D is minimal, we can extract from the premise $\Gamma \dashv (v_1, v_2) : t_1 \times t_2$ a collection of derivations of the judgements $\Gamma \dashv v_1 : s_i$ and $\Gamma \dashv v_2 : s'_i$ for $i \in I$, such that there exists some instantiations $\Sigma_i$ such that $\bigwedge_{i \in I}(s_i \times s'_i)\Sigma_i \le t_1 \times t_2$. We thus have $\bigwedge_{i \in I} s_i\Sigma_i \le t_1$, as none of the $\{s'_i\}_{i \in I}$ can be $\emptyset$ (this would contradict Proposition I.23 as $v_2$ is a value).

Therefore, we can conclude this case by using a [INST∧≤] pattern with the premises $\{\Gamma \dashv v_1 : s_i\}_{i \in I}$ in order to derive $\Gamma \dashv v_1 : t_1$.

[×E2] Similar to the previous case.

[⊤] We have $e \equiv e_1\{e_2/x\}$ for some expressions $e_1$ and $e_2$, and thus $e' \equiv (e_1\{e_2/x\})\{e'_o/e_o\}$.

We have the following premises:
(1) Definition premise: $\Gamma \vdash e_2 : s$

(2) Body premises: $\forall i \in I$. $\Gamma, x : s \wedge u_i \vdash e_1 : t$

As $D$ is minimal, we know that $e_2$ cannot be a value. Also, we know that $e_o$ does not contain $x$ as a free variable (otherwise there would be no occurrence of $e_o$ in $e_1\{e_2/x\}$). Consequently, $e'_o$ does not contain $x$ neither, because a reduction step cannot introduce a new free variable. There are several cases:

* $e_o$ does not contain $e_2$ and $e_2$ does not contain $e_o$. In this case, we have: $e' \equiv (e_1\{e_2/x\})\{e'_o/e_o\} \equiv (e_1\{e'_o/e_o\})\{e_2/x\}$. Thus, we can easily conclude by keeping the definition premise of the $[\forall]$ node and applying the induction hypothesis on the body premises.

* $e_2$ contains $e_o$. In this case, we pose $e'_2 = e_2\{e'_o/e_o\}$. We have $e' \equiv (e_1\{e_2/x\})\{e'_o/e_o\} \equiv (e_1\{e'_o/e_o\})\{e'_2/x\}$. We can derive $\Gamma \vdash e'_2 : s$ by induction on the definition premise, and $\Gamma, x : s \wedge u_i \vdash e_1\{e'_o/e_o\} : t$ for all $i \in I$ by induction on the body premises. Thus, we can derive $\Gamma \vdash (e_1\{e'_o/e_o\})\{e'_2/x\} : t$ using a $[\forall]$ node.

* $e_o$ contains $e_2$ as a strict sub-expression. In this case, we pose $e_\bullet = e_o\{x/e_2\}$ and $e'_\bullet = e'_o\{x/e_2\}$. We know that $e_1$ does not contain any occurrence of $e_2$ (because $D$ is minimal), and thus no occurrence of $e_o$ neither. Consequently, we have $e' \equiv (e_1\{e_2/x\})\{e'_o/e_o\} \equiv (e_1\{e'_\bullet/e_\bullet\})\{e_2/x\}$.

As $e_2$ is not a value, it can only appear in $e_o$ inside of a $\lambda$-abstraction, and/or inside of a branch of a typecase: otherwise, $e_o$ would not be reducible.

Thus, we can deduce that $e_\bullet = e_o\{x/e_2\} \rightsquigarrow e'_o\{x/e_2\} = e'_\bullet$. Consequently, we can easily conclude by keeping the definition premise of the $[\forall]$ node and applying the induction hypothesis on the body premises.

[0] We have $e \equiv (e_1 \in \tau) ? e_2 : e_3$ for some $e_1, e_2$ and $e_3$. As values cannot have the type $\emptyset$ (Proposition I.23), we know that $e_1$ is not a value. Thus, $e' \equiv (e_1\{e'_o/e_o\} \in \tau) ? e_2\{e'_o/e_o\} : e_3\{e'_o/e_o\}$. We can derive $\Gamma \vdash e_1\{e'_o/e_o\} : \emptyset$ by proceeding inductively on the premise, and then we can derive $\Gamma \vdash e' : \emptyset$ by using $[0]$.

[e_1] We have $e \equiv (e_1 \in \tau) ? e_2 : e_3$ for some $e_1, e_2$ and $e_3$. There are three cases: $e' \equiv (e_1\{e'_o/e_o\} \in \tau) ? e_2\{e'_o/e_o\} : e_3\{e'_o/e_o\}$ We can easily conclude by proceeding inductively on the premises.

$e' \equiv e_2$ The second premise, unchanged, allows us to conclude.

$e' \equiv e_3$ This case is impossible. Indeed, it implies that $e_1$ is a value, and as $\Gamma \vdash e_1 : \tau$ (first premise), we can deduce using Proposition I.23 that $e_1 \in \tau$, which contradicts $e \rightsquigarrow e_3$.

[e_2] Similar to the previous case.

□

**THEOREM I.31 (SUBJECT REDUCTION).** If $\Gamma \vdash e : t$ with $e$ a ground expression and if $e \rightsquigarrow e'$, then $\Gamma \vdash e' : t$.

**PROOF.** Using the normalisation theorem (Theorem I.22) and the Lemma I.29, we can build a minimal derivation for $\Gamma \vdash e : t$.

Moreover, the root of the reduction step $e \rightsquigarrow e'$ is a $[\kappa]$ node, with its premise being of the form $e_o \rightsquigarrow e'_o$, and with $e' \equiv e\{e'_o/e_o\}$.

Thus, by using Lemma I.30, we obtain $\Gamma \vdash e' : t$. □

□

### I.2.3 Progress.

**LEMMA I.32 (PROGRESS).** If $D$ is a minimal derivation for $\Gamma \vdash e : t$, and if there is no evaluation context $E$ and variable $x/x$ such that $e \equiv E[x/x]$, then either $e$ is a value or $\exists e' : e \rightsquigarrow e'$.
**PROOF.** We proceed by structural induction on $D$. We consider the root of the derivation:

[CONST] Trivial ($e$ is a value).

[Ax_λ] Impossible case (contradict the hypotheses).

[Ax_ν] Impossible case (contradict the hypotheses).

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


 Trivial (by induction on the premise).

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

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

[×I] We have $e \equiv (e_1, e_2)$ for some expressions $e_1$ and $e_2$.

• If $e_1$ is not a value, and as we have $\forall E, x/x. e_1 \neq E[x/x]$, we know by applying the induction hypothesis that $e_1$ can be reduced. Thus, $e$ can also be reduced under the evaluation context ( [], $e_2$).

• If $e_1$ is a value, then we can apply the induction hypothesis on the second premise (as $e_1$ is a value, we know that $\forall E, x/x. e_2 \neq E[x/x]$). It gives that either $e_2$ is a value or it can be reduced. We can easily conclude in both cases: if $e_2$ is a value, then $e$ is also a value, otherwise, $e$ can be reduced under the evaluation context ($e_1$, []).

[→E] We have $e \equiv e_1 e_2$ for some expressions $e_1$ and $e_2$, with $\Gamma \vdash e_1 : s \rightarrow t$ and $\Gamma \vdash e_2 : s$.

• If $e_1$ is not a value, and as we have $\forall E, x/x. e_1 \neq E[x/x]$, we know by applying the induction hypothesis that $e_1$ can be reduced. Thus, $e$ can also be reduced under the evaluation context [] $e_2$.

• If $e_1$ is a value, we can apply Proposition I.23 on it: as $\Gamma \vdash e_1 : \emptyset \rightarrow 1$, it implies that $e_1 \in \emptyset \rightarrow 1$ and thus $e_1 \equiv \lambda x. e_\lambda$ for some $e_\lambda$. Moreover, we can apply the induction hypothesis on the second premise (as $e_1$ is a value, we know that $\forall E, x/x. e_2 \neq E[x/x]$). It gives that either $e_2$ is a value or it can be reduced. We can easily conclude in both cases: if $e_2$ is a value, then $e$ can be reduced using the rule 7, otherwise, $e$ can be reduced under the evaluation context $e_1$ [].

[×E₁] We have $e \equiv \pi_1 e_1$ for some $e_1$, with $\Gamma \vdash e_1 : t \times s$. By applying the induction hypothesis on the premise, we know that $e_1$ is either a value or it can be reduced. If $e_1$ can be reduced, then $e$ can also be reduced under the evaluation context $\pi_1$ []. Otherwise, as $\Gamma \vdash e_1 : 1 \times 1$, we can apply Proposition I.23 on it, yielding $e_1 \in 1 \times 1$. Thus, $e_1 \equiv (v_1, v_2)$ for some values $v_1$ and $v_2$, and consequently $e$ can be reduced using the rule 8.

[×E₂] Similar to the previous case.

[V] We have $e \equiv e_1\{e_2/x\}$ for some $e_1$ and $e_2$, with $\Gamma \vdash e_2 : s$ and $\forall i \in I. \Gamma, x : s \wedge u_i \dashv e_1 : t$. There are two cases:

• There exists an evaluation context $E$ such that $e_1 \equiv E[x]$. In this case, we know that $\forall E', y/\gamma. e_2 \neq E'[y/\gamma]$, otherwise we would have $e \equiv E[E'[y/\gamma]]$. Thus, we can apply the induction hypothesis on the definition premise. It gives that either $e_2$ is a value or it can be reduced. As $D$ is minimal, $e_2$ cannot be a value and thus $e_2$ can be reduced. Consequently, $e$ can also be reduced under the evaluation context $E$.

• There is no evaluation context $E$ such that $e_1 \equiv E[x]$. In this case, we apply the induction hypothesis on one of the body premises. It gives that either $e_1$ is a value or it can be reduced. We can easily conclude in both cases: if $e_1$ is a value, then $e$ is also a value, otherwise, $e$ can be reduced.

[O] We have $e \equiv (e_1 \in \tau) ? e_2 : e_3$ for some $e_1, e_2$ and $e_3$, with $\Gamma \vdash e_1 : \emptyset$. As values cannot have the type $\emptyset$ (Proposition I.23), we know that $e_1$ is not a value. Thus, by applying the induction
hypothesis on the premise, we know that $e_1$ can be reduced. Consequently, $e$ can be reduced under the evaluation context ($\boxed{\phantom{\tau}} \in \tau$) ? $e_2 : e_3$.

[e1] We have $e \equiv (e_1 \in \tau) ? e_2 : e_3$ for some $e_1, e_2$ and $e_3$, with $\Gamma \vdash e_1 : \tau$. We thus have $e_1 \in \tau$ (Proposition I.23). By applying the induction hypothesis on the first premise, we know that $e_1$ is either a value or it can be reduced. If $e_1$ is a value, then $e$ can be reduced using the rule 10. Otherwise, $e_1$ can be reduced and thus $e$ can also be reduced under the evaluation context ($\boxed{\phantom{\tau}} \in \tau$) ? $e_2 : e_3$.

[e2] Similar to the previous case. □

**THEOREM I.33 (PROGRESS).** If $\emptyset \neq e : t$ with $e$ a ground expression, then either $e$ is a value or $\exists e'. e' \not\sim_{\emptyset} e'$.

**PROOF.** Using the normalisation theorem (Theorem I.22) and the Lemma I.29, we can build a minimal derivation for $\emptyset \neq e : t$.

Moreover, we can deduce from $\emptyset \neq e : t$ that there is no evaluation context $E$ and lambda variable $x/\lambda$ such that $e \equiv E[x/\lambda]$. Thus, we can conclude using Lemma I.32. □

**I.2.4 Type Safety for Programs.** Now that we expressed subject reduction and progress for the parallel semantics on expressions, we extend it to programs, still using the parallel semantics. Then, we will deduce from it a type safety theorem on programs for the parallel semantics.

**LEMMA I.34 (WEAK MONOTONICITY).** For derivation $D$ of $\Gamma \vdash e : t$ and environment $\Gamma'$ such that $\Gamma' \le \Gamma$, $D$ can be transformed into a derivation of $\Gamma' \vdash e : t$ just by adding $\le$ nodes.

**PROOF.** Straightforward induction on the derivation $\Gamma \vdash e : t$, where each $[Ax_\vee]$ and $[Ax_\lambda]$ node is replaced by a $\le$ node with the $[Ax_\vee]$ or $[Ax_\lambda]$ node as premise. □

**LEMMA I.35 (ELIMINATION OF 
 NODES).** For any canonical form derivation $D$ of $\Gamma \vdash e : t$ and set of substitutions $\Sigma$, $D$ can be transformed into a derivation $D'$ of $\Gamma \Sigma' \vdash e : t\Sigma$, for some $\Sigma'$, and such that $D'$ does not contain any 
 node.

**PROOF.** We proceed by structural induction on the derivation $D$ (with $D$ being a canonical form derivation).

If the root of $D$ is a $[Ax_\vee]$ node, we can directly conclude by choosing $\Sigma' = \Sigma$.

Otherwise, if the root $D$ is a $[\vee]$ node, doing a substitution $e\{e'/x\}$, we first proceed inductively on its body premises (which all are canonical form derivations). It yields some derivations $\Gamma \Sigma'_i x : s \Sigma'_i \wedge u_i \vdash e : t\Sigma$ for $i \in I$. We consider the set of substitutions $\Sigma' = \bigcup_{i \in I} \Sigma'_i$.

Now, let's try to derive $\Gamma \Sigma'' \vdash e' : s'$, for some $\Sigma''$ and $s'$, with $s' \le s\Sigma' \le (s\Sigma'_i \text{ for every } i \in I)$. For that, we consider the definition premise of $D$, deriving $\Gamma \vdash e' : s$, and apply the following process on it:

* If its root is a $[\wedge]$ node, we apply inductively this process to each premise $\Gamma \vdash e' : s_j$ (with $\bigvee_{j \in J} s_j \simeq s$) in order to derive some $\Gamma \Sigma_j'' \vdash e' : s'_j$, with $s'_j \le s\Sigma'$. We then consider $\Sigma'' = \bigcup_{j \in J} \Sigma_j''$, and derive for each $j \in J$ $\Gamma \Sigma'' \vdash e' : s'_j$ using Lemma I.34. Finally, we intersect the those derivations with a $[\wedge]$ node.
Let $\sigma''$ be an injective substitution mapping every polymorphic type variable appearing in the image of at least one of the substitutions $\sigma' \in \Sigma'$ and $\phi$ to a fresh monomorphic type variable (and being the identity for any other type variable). From $\Gamma\Sigma', x : (s\phi)\Sigma' \dashv e : t$, we can derive a derivation of $(\Gamma\Sigma')\sigma''$, $x : ((s\phi)\Sigma')\sigma'' \dashv e : t\sigma''$ simply by renaming the type variables everywhere according to $\sigma''$. This is only possible because the derivation does not contain any 
 node (substituting a polymorphic type variable by a monomorphic one could invalidate 
 nodes). By monotonicity (Lemma 1.4), we get $\Gamma, x : ((s\phi)\Sigma')\sigma'' \dashv e : t\sigma''$.

Now, we consider the set of substitutions $\{\phi_i\}_{i \in I} \stackrel{\text{def}}{=} \{\sigma'' \circ \sigma' \circ \phi \mid \sigma' \in \Sigma'\}$. For any $i \in I$, we can decompose $\phi_i$ into two substitutions, $\psi_i \stackrel{\text{def}}{=} \sigma_i|_{\nu_M}$ and $\sigma_i \stackrel{\text{def}}{=} \sigma_i|_{\nu_P}$. Note that $\forall i \in I$. $\psi_i\#\Gamma$ (it follows from $\phi\#\Gamma$). Rewriting the previous judgement with these new notations gives $\Gamma, x : \bigwedge_{i \in I}(s\psi_i)\sigma_i \dashv e : t\sigma''$.

Using Lemma 1.36 on the derivation of $\Gamma \dashv e' : s$, we can derive, for any $i \in I$, $\Gamma \dashv e' : s\psi_i$ (we recall that $\psi_i\#\Gamma$, and thus $\Gamma\psi_i \cong \Gamma$). Using a 
 node, we can then derive $\Gamma \dashv e' : (s\psi_i)\sigma_i$ for any $i \in I$. Regrouping those derivations with a $[\wedge]$ node gives $\Gamma \dashv e' : \bigwedge_{i \in I}(s\psi_i)\sigma_i$.

Finally, using the substitution lemma (Lemma 1.24) on $\Gamma, x : \bigwedge_{i \in I}(s\psi_i)\sigma_i \dashv e : t\sigma''$ and $\Gamma \dashv e' : \bigwedge_{i \in I}(s\psi_i)\sigma_i$, we get a derivation for $\Gamma \dashv e\{e'/x\} : t\sigma''$. We recall that the substitution $\sigma''$ is injective and thus reversible, with its inverse $\phi'$ being such that $\phi'\#\Gamma$ (as the image of $\sigma''$ is only composed of fresh monomorphic type variables). Thus, we have $(t\sigma'')\phi' \cong t$, which concludes the proof. $\square$

We now have all the results necessary to prove the type safety of programs for the parallel semantics. The parallel semantics is extended to programs in a straightforward way:

$$ \begin{array}{l@{\qquad}l} \textbf{Reduction rule} & \text{let } x=v; p \rightsquigarrow_{\mathcal{P},p_r} p\{v/x\} \\ \textbf{Evaluation Context} & P ::= [] | \text{let } x= [] ; p \end{array} \qquad \frac{e \rightsquigarrow \rho \ e'}{P[e] \rightsquigarrow_{\mathcal{P},p_r} P[e']}

**THEOREM I.38 (SUBJECT REDUCTION FOR PROGRAMS).** If $\Gamma \vdash p : t$ and $p \rightsquigarrow_{\mathcal{P},p_r} p'$, then $\Gamma \vdash p' : t$.

**PROOF.** Direct consequence of Theorem I.31 and Lemma I.37. $\square$

**THEOREM I.39 (PROGRESS FOR PROGRAMS).** If $\emptyset \vdash p : t$, then either $p$ is a value or $\exists p' : p \rightsquigarrow_{\mathcal{P},p_r} p'$.

**PROOF.** Direct consequence of Theorem I.33. $\square$

**THEOREM I.40 (TYPE SAFETY FOR THE PARALLEL SEMANTICS).** For any program $p$, if $\emptyset \vdash p : t$, then either $p \rightsquigarrow_{\mathcal{P},p_r} v$ with $\emptyset \vdash p : t$ or $e \rightsquigarrow_{\mathcal{P},p_r} \infty$.

**PROOF.** Straightforward consequence of Theorem I.38 and Theorem I.39. $\square$

### 1.2.5 Type Safety for the Source Semantics.
The final step is to deduce a type safety theorem for the source semantics (Figure 1) from the type safety theorem for the parallel semantics. In order to help comparing the two reduction semantics, we introduce again another reduction semantics $\rightsquigarrow_C$ on expressions that can perform a reduction $\rightsquigarrow_\tau$ under any context $C$ (not just an evaluation context):

$$ C ::= [] | C e | e C | (C, e) | (e, C) | \pi_i C \qquad \frac{e \rightsquigarrow_\tau e'}{C[e] \rightsquigarrow_C C[e']} $$

**DEFINITION I.41.** We say that a context $C_1$ is a subcontext of $C_2$, noted $C_1 \leq C_2$, if and only if there exists a context $C'_1$ such that $C_2 \equiv C_1[C'_1]$.

**LEMMA I.42.** For any expressions $e_1$ and $e_3$, if we have a chain $e_1 \rightsquigarrow_C^* e_3$ such that at least one of the reduction steps happen under an evaluation context, then there exists an expression $e_2$ such that $e_1 \rightsquigarrow e_2$ and $e_2 \rightsquigarrow_C^* e_3$.
**PROOF.** Let $e_1$ and $e_4$ two expressions such that $e_1 \rightsquigarrow_C^* e_4$, where at least one of the reduction steps happen under an evaluation context.

Let's consider the first reduction step $e_2 \rightsquigarrow_C e_3$ happening under an evaluation context. We have $e_1 \rightsquigarrow_C^* e_2$ (with no reduction step happening under an evaluation context) and $e_3 \rightsquigarrow_C^* e_4$. Moreover, we have $e_2 \equiv E[e'_2]$ and $e_3 \equiv E[e'_3]$ for some evaluation context $E$ and expressions $e'_2$ and $e'_3$ such that $e'_2 \rightsquigarrow_T e'_3$.

No reduction step in $e_1 \rightsquigarrow_C^* e_2$ happen under a context $C$ such that $C \le E$: otherwise, it would also be an evaluation context, contradicting the fact that $e_2 \rightsquigarrow_C e_3$ is the first reduction step happening under an evaluation context. Consequently, we can "reverse" in $E$ and $e'_2$ the reduction steps happening in $e_1 \rightsquigarrow_C^* e_2$ (one after the other, in reverse order):

* If a reduction step happens under a context $C$ such that $E \le C$, it only involves $e'_2$, we can thus apply the reverse rewriting to $e'_2$. After that, the expression we get is still reducible at top-level, as the reduction step that has been reversed cannot happen under an evaluation context (no reduction step in $e_1 \rightsquigarrow_C^* e_2$ can happen under an evaluation context).

* Otherwise, if a reduction step happens under a context $C$ such that $C \not\le E$ and $E \not\le C$, it only involves $E$, we can thus apply the reverse rewriting to $E$. After that, the new context we get is still an evaluation context, as the reduction step that has been reversed cannot happen under an evaluation context (no reduction step in $e_1 \rightsquigarrow_C^* e_2$ can happen under an evaluation context).

After this reversing process, we get a new evaluation context $E'$ and expression $e'_1$ such that $e_1 \equiv E'[e'_1]$ and $e'_1 \rightsquigarrow_T e'_2$ for some $e'_2$ such that $E'[e'_2] \rightsquigarrow_C^* E[e'_2]$.

Consequently, we have $e_1 \equiv E'[e'_1] \rightsquigarrow E'[e'_2]$, and $E'[e'_2] \rightsquigarrow_C^* E[e'_2] \equiv e_3 \rightsquigarrow_C^* e_4$, which concludes the proof. □

**LEMMA I.43.** For any expressions $e_1, e_2$ and $e_3$, if $e_1 \rightsquigarrow_C^* e_2 \rightsquigarrow_T e_3$, then there exists an expression $e'_1$ such that $e_1 \rightsquigarrow e'_1 \rightsquigarrow_C^* e_3$.

**PROOF.** The step $e_2 \rightsquigarrow_T e_3$ can be decomposed into several $\rightsquigarrow_C$ steps with at least one happening under an evaluation context. Thus, this lemma is an immediate consequence of Lemma I.42 applied on the chain $e_1 \rightsquigarrow_C^* e_2 \rightsquigarrow_C^* e_3$. □

**LEMMA I.44.** For any expression $e$ and value $v$, if $e \rightsquigarrow_C^* v$ then either $e \rightsquigarrow \infty$ or there exists a value $v'$ such that $e \rightsquigarrow^* v' \rightsquigarrow_C^* v$.

**PROOF.** If $e$ is not already a value, then there must be at least one step in $e \rightsquigarrow_C^* v$ that happen under an evaluation context (it is not possible for $v$ to be a value otherwise). We can thus apply Lemma I.42 successively, starting on $e \rightsquigarrow_C^* v$ and continuing until the remaining $e' \rightsquigarrow_C^* v$ chain is such that $e'$ is a value. If this process terminates, it builds a chain $e \rightsquigarrow^* v'$ with $v' \rightsquigarrow_C^* v$, otherwise it builds $e \rightsquigarrow \infty$. □

**LEMMA I.45.** For any expression $e_1, e_2$, and value $v$, if $e_1 \rightsquigarrow_C^* e_2 \rightsquigarrow_T v$ then there exists $v'$ such that $e_1 \rightsquigarrow^* v' \rightsquigarrow_C^* v$ or $e_1 \rightsquigarrow \infty$.

**PROOF.** By induction on the number of steps in $e_2 \rightsquigarrow_T v$, we prove using Lemma I.43 that $e_1 \rightsquigarrow^* e' \rightsquigarrow_C^* v$ for some $e'$. Then, we conclude by applying Lemma I.44 on $e' \rightsquigarrow_C^* v$. □

**LEMMA I.46.** For any expression $e_1$ and $e_2$, if $e_1 \rightsquigarrow_C^* e_2 \rightsquigarrow_T \infty$ then $e_1 \rightsquigarrow \infty$.

**PROOF.** We can arbitrarily extend a chain $e_1 \rightsquigarrow \dots \rightsquigarrow$ using Lemma I.43. □

The semantics $\rightsquigarrow_C$ is extended into a semantics $\rightsquigarrow_{C,Pr}$ for programs, with an extended context allowing to perform a reduction under any top-level definition of the program:
$$ C_{Pr} ::= [] | \text{let } x = [] ; p | \text{let } x = e ; C_{Pr} \qquad \frac{e \rightsquigarrow e'}{C_{Pr}[C[e]] \rightsquigarrow_{C,Pr} C_{Pr}[C[e']]} $$

LEMMA I.47. For any program $p_1, p_2$, and value $v$, if $p_1 \rightsquigarrow_{C,Pr} p_2 \rightsquigarrow_{P,Pr} v$ then there exists $v'$ such that $p_1 \rightsquigarrow_{Pr} v' \rightsquigarrow_{C,Pr} v$ or $p_1 \rightsquigarrow_{Pr}^{\infty}$.

PROOF. Straightforward induction on the number of top-level definitions in $p_2$, using Lemma I.45 (note that $p_1$ and $p_2$ must have the same number of top-level definitions as $p_1 \rightsquigarrow_{C,Pr} p_2$). $\square$

LEMMA I.48. For any program $p_1$ and $p_2$, if $p_1 \rightsquigarrow_{C,Pr} p_2 \rightsquigarrow_{P,Pr}^{\infty}$ then $p_1 \rightsquigarrow_{Pr}^{\infty}$.

PROOF. Straightforward induction on the number of top-level definitions in $p_2$, using Lemma I.46 (note that $p_1$ and $p_2$ must have the same number of top-level definitions as $p_1 \rightsquigarrow_{C,Pr} p_2$). $\square$

LEMMA I.49. For any values $v_1$ and $v_2$ such that $v_1 \rightsquigarrow_{C}^{*} v_2$, if $v_2 \in \tau$ then $v_1 \in \tau$.

PROOF. As $v_1$ is a value, every reduction step in $v_1 \rightsquigarrow_{C}^{*} v_2$ can only happen under a $\lambda$-abstraction. Given that the $\in$ relation ignores the body of $\lambda$-abstractions $((\lambda x.e) \in \emptyset \rightarrow 1$ for any $e)$, none of the reduction steps in $v_1 \rightsquigarrow_{C}^{*} v_2$ can change the relation $\cdot \in \tau$. $\square$

THEOREM I.50 (TYPE SAFETY FOR THE SOURCE SEMANTICS). For any program $p$, if $\emptyset \vdash_{Pr} p : \tau$, then either $p \rightsquigarrow_{Pr}^{*} v$ with $v \in \tau$ or $p \rightsquigarrow_{Pr}^{\infty}$.

PROOF. Straightforward combination of the type safety for the parallel semantics (Theorem I.40) with the Lemmas I.47 and I.48. In the case where we get $p \rightsquigarrow_{Pr}^{*} v$, for some value $v$ such that there exists $v'$ such that $v \rightsquigarrow_{C}^{*} v'$ and $\emptyset \vdash_{Pr} v' : \tau$, we can deduce $\emptyset \vdash v' : \tau$, then $v' \in \tau$ using Proposition I.23, and finally $v \in \tau$ using Lemma I.49. $\square$

## I.3 Algorithmic Type System

### I.3.1 Maximal Sharing Canonical Form.
This section applies to definitions of Appendix E.

As defined in Section I.1, we consider that expressions of the source language can contain binding variables. In particular, the unwinding operator $[.]$ can be used on atoms and canonical forms containing free binding variables. An expression without binding variables is called ground expression.

PROPOSITION I.51. For any ground expression of the source language $e$, $[\text{term}([e]]] \equiv e$.

PROOF. Straightforward structural induction on $e$. $\square$

PROPOSITION I.52. If $\kappa \equiv_{\kappa} \kappa'$, then $[\kappa] \equiv_{\alpha} [\kappa']$.

PROOF. If a reordering, as defined in Definition 3.1, applies at top-level on the expression $\text{bind } x_1 = a_1 \text{ in } \text{bind } x_2 = a_2 \text{ in } \kappa$, the unwinding remains unchanged: as $x_1 \notin \text{fv}(a_2)$ and $x_2 \notin \text{fv}(a_1)$, we have $\kappa\{a_1/x_1\}\{a_2/x_2\} \equiv \kappa\{a_2/x_2\}\{a_1/x_1\}$.

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]]$ (with $C$ denoting an arbitrary context). $\square$

PROPOSITION I.53 (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. We will show that $\kappa_2$ can be transformed into $\kappa_1$ just with $\alpha$-renaming and reordering of independent bindings (as specified in the definition of $\equiv_{\kappa}$).

In this proof, we represent partially unwinded canonical forms by a pair $(B, e)$, where $B$ is a binding context and $e$ an expression. With this representation, the unwinding of $(B, e)$ is $eB$, but for clarity we can also use the notation $[B, e]$.
Let $(B_1, x_1)$ be the representation of $\kappa_1$, with $B_1$ representing its top-level definitions and $x_1$ its final binding variable, and $(B_2, x_2)$ be the representation of $\kappa_2$. Formally, we have term$(B_1, x_1) \equiv \kappa_1$ and term$(B_2, x_2) \equiv \kappa_2$.

As $\lceil \kappa_1 \rceil \equiv_\alpha \lceil \kappa_2 \rceil$, we have $\lceil (B_1, x_1) \rceil \equiv_\alpha \lceil (B_2, x_2) \rceil$. By $\alpha$-renaming, we can assume that $x_1 = x_2 = x$ and $\lceil (B_1, x) \rceil = \lceil (B_2, x) \rceil$.

Now, let's prove the property below, from which Proposition 1.53 can be deduced. Let $B_1$ and $B_2$ two binding contexts, and $e$ an expression such that:

* $\lceil (B_1, e) \rceil \equiv \lceil (B_2, e) \rceil$

* The body of $\lambda$-abstractions in $B_1$ and $B_2$ are in MSC-form (Definition 3.2)

* Both $B_1$ and $B_2$ satisfy the following properties (corresponding to the MSC-form properties applied to the top-level definitions), written here for a binding context $B$:

(1) if $(x_1, a_1)$ and $(x_2, a_2)$ are distinct definitions in $B$, then $a_1 \neq_k a_2$

(2) for any definition $(x, \lambda z. \kappa)$ in $B$, any binding bind $y = a$ in $\kappa$ in $\kappa$ is such that $fv(a) \notin fv(\lambda z. \kappa)$

(3) if $B$ contains a definition $(x, a)$, then $x$ is a free variable of one of the next definitions in $B$ or of $e$

Then, we can transform $B_2$ into $B_1$ just with $\alpha$-renaming, reordering of independent definitions, and replacement of an atom by $a \equiv_\kappa$-equivalent one.

We prove this property by induction on the total number of atoms appearing in $B_1$ (by counting top-level atoms as well as the sub-atoms they contain).

The base case ($B_1 = \varepsilon$) is trivial: as $\lceil (B_2, e) \rceil \equiv \lceil (B_1, e) \rceil \equiv \lceil (\varepsilon, e) \rceil \equiv e$, we deduce with Property 3 of MSC-forms that $B_2 = \varepsilon$.

For the inductive case, let's consider $B_1 = B'_1$; $(x, a_1)$.

With property 3 of MSC-forms, we know that $x$ appears in $e$. As $\lceil (B_1, e) \rceil \equiv \lceil (B_2, e) \rceil$, we can deduce that $\lceil (B_1, x) \rceil \equiv \lceil (B_2, x) \rceil$. Thus, $B_2$ must also feature a definition for $x$, let's call $a_2$ the associated atom. We move in $B_2$ the definition $(x, a_2)$ at the end (if not already), it gives $B_2 = B'_2$; $(x, a_2)$. We then have $\lceil (B'_1, a_1) \rceil \equiv \lceil (B'_2, a_2) \rceil$. As every kind of atom introduces a different syntactic construction, we can deduce that $a_1$ and $a_2$ are atoms of the same kind.

* If $a_1$ and $a_2$ are atoms that are not $\lambda$-abstractions and that do not contain any binding variable (constants, lambda variables), we directly have $a_1 \equiv a_2$.

* If $a_1$ and $a_2$ are atoms that are not $\lambda$-abstractions and that contain only one binding variable (projections), we can $\alpha$-rename binding variables in $B_2$ so that $a_1 \equiv a_2$.

* If $a_1$ and $a_2$ are atoms that are not $\lambda$-abstractions and that contain two binding variables $x$ and $y$ (applications, pairs), we consider two cases:

- If $\lceil (B'_1, x) \rceil \equiv_\alpha \lceil (B'_1, y) \rceil$, let's show that we necessarily have $x = y$. We consider the binding context $B_x$, which is a cleaned version of $B'_1$ where all the definitions that are not related (directly or indirectly) to $x_1$ have been removed. Similarly, we consider the binding context $B_y$ where the definitions unrelated to $y$ have been removed. Then, we apply the induction hypothesis to the binding contexts $B_x$, $B_y\{x/y\}$ and the expression $x$. This tells us that $B_x$ and $B_y$ are equivalent modulo reordering of the definitions, $\alpha$-renaming and $\equiv_\kappa$-transformation of atoms. Thus, according to the property 1 of MSC-forms, $x$ and $y$ cannot have two distinct definitions in $B'_1$, and thus $x = y$. The same reasoning can be done for $a_2$, and thus we deduce that both $a_1$ and $a_2$ contain the same binding variable twice. Thus, we can $\alpha$-rename binding variables in $B_2$ so that $a_1 \equiv a_2$.

- Otherwise, $x$ and $y$ must be different, and the same applies to $a_2$. Thus, we can $\alpha$-rename binding variables in $B_2$ so that $a_1 \equiv a_2$.
* If $a_1$ and $a_2$ are typecases (containing 3 binding variables), we proceed similarly to the previous case to obtain $a_1 \equiv a_2$.

* In the case where $a_1$ and $a_2$ are $\lambda$-abstractions, let's say $\lambda x. \kappa_1$ and $\lambda x. \kappa_2$, we note $(B_{x_1}, x_1)$ and $(B_{x_2}, x_2)$ the representations of $\kappa_1$ and $\kappa_2$ respectively. We now consider the representation $(B'_1; B_{x_1}, \lambda x. x_1)$ and remove from it all the unused definitions (i.e. not related to $x_1$), it gives us a new representation $(B''_1, \lambda x. x_1)$. We do the same for $(B'_2; B_{x_2}, \lambda x. x_2)$, it gives a new representation $(B''_2, \lambda x. x_2)$. Then, we use the induction hypothesis on $B'_1, B''_2$ and $\lambda x. x_1$. It gives us that $B''_1$ and $B''_2$ are equivalent modulo reordering of the definitions, $\alpha$-renaming and $\equiv_\kappa$-transformation of the atoms. By using the property 2 of MSC-forms, we can deduce that $B_{x_1}$ and $B_{x_2}$ are equivalent modulo reordering of the definitions, $\alpha$-renaming and $\equiv_\kappa$-transformation of the atoms. Thus, we can $\alpha$-rename $B_2$ and $\equiv_\kappa$-transform some of its atoms so that $B_{x_1} \equiv B_{x_2}$, and thus $a_1 \equiv a_2$.

In any case, we get $a_1 \equiv a_2 \equiv a$, thus the last definition of $B_1$ is the same as the last definition of $B_2$. The same can be proven for the previous definitions by using the induction hypothesis on $B'_1, B'_2$ and $e\{a/x\}$. $\square$

**PROPOSITION I.54.** If $\kappa \vdash \kappa'$, then $\lceil \kappa \rceil \equiv_\alpha \lceil \kappa' \rceil$.

**PROOF.** Similar to Proposition I.52. $\square$

**PROPOSITION I.55 (NORMALISATION).** There is no infinite chain $\kappa_1 \dashv \kappa_2 \dashv \dots$

**PROOF.** Let $n$ be the maximal number of nested $\lambda$-abstractions in $\kappa_1$. We call depth of a binding the number of nested $\lambda$-abstractions 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))$.

For any chain $\kappa_1 \dashv \kappa_2 \dashv \dots$, the sequence $S(\kappa_1), S(\kappa_2), \dots$ is strictly decreasing with respects to the lexicographic order. Thus $\kappa_1 \dashv \kappa_2 \dashv \dots$ cannot be infinite. $\square$

**PROPOSITION I.56.** If $\kappa \not\vdash$ (i.e., no $\vdash$ rule apply on $\kappa$), then $\kappa$ is an MSC-form.

**PROOF.** We assume $\kappa \not\vdash$ and show that all 3 MSC properties are satisfied.

The property 3 (no unused bindings) is trivially verified: any binding that does not satisfy this property can directly be eliminated with the rule 4. As the rule 4 does not apply, this property must be satisfied.

Now, we focus on the property 2 (extrusion of bindings). We assume that there exists a sub-expression $\lambda x. \kappa_1$ of $\kappa$ and a sub-expression bind $y = a$ in $\kappa_2$ of $\kappa_1$ such that $fv(a) \subseteq fv(\lambda x. \kappa_1)$. We know that $a$ does not depend on $x$, otherwise $x$ would be in $fv(a)$ and not in $fv(\lambda x. \kappa_1)$. Thus, we can reorder the binding $y$ (6) in the first position of its inner-most containing lambda-abstraction, and then apply the rule 5 on it, which contradicts $\kappa \not\vdash$. Consequently, the property 2 is satisfied.

Finally, we show that the property 1 (sharing) is also satisfied. We assume that there are two distinct bindings bind $x_1 = a_1$ in \dots and bind $x_2 = a_2$ in \dots such that $a_1 \equiv_\kappa a_2$. As the property 2 is satisfied, and as $fv(a_1) = fv(a_2)$, we know that these two bindings are in the same $\lambda$-abstraction. Thus, we can reorder them (6) to be the one next to the other so that the rule 3 is applicable, which contradicts $\kappa \not\vdash$. Thus, the property 1 is satisfied. $\square$

**PROPOSITION I.57 (CONFLUENCE).** Let $\kappa_1, \kappa_2$ and $\kappa'_2$ such that $\kappa_1 \dashv^* \kappa_2$ and $\kappa_1 \dashv^* \kappa'_2$. Then, there exists $\kappa_3$ and $\kappa'_3$ such that $\kappa_2 \dashv^* \kappa_3, \kappa'_2 \dashv^* \kappa'_3$, and $\kappa_3 \equiv_\kappa \kappa'_3$.

**PROOF.** Immediate consequence of Proposition I.55 (normalisation), Proposition I.54 (preservation of $\lceil \cdot \rceil$), Proposition I.56 ($\not\vdash$ implies MSC-form), and Proposition I.53 (equivalence of MSC-forms). $\square$
### 1.3.2 Soundness.
See Appendix G for the full algorithmic system, without the rules for extensions.

**LEMMA 1.58 (MONOTONICITY).**

If $\Gamma \vdash_{\mathfrak{A}} [\kappa | \mathfrak{k}] : t$ and $\Gamma' \leq_P \Gamma$, then $\exists \mathfrak{k}', t'$. $\Gamma' \vdash_{\mathfrak{A}} [\kappa | \mathfrak{k}'] : t'$ with $t' \leq_P t$.

If $\Gamma \vdash_{\mathfrak{A}} [a | \emptyset] : t$ and $\Gamma' \leq_P \Gamma$, then $\exists \emptyset', t'$. $\Gamma' \vdash_{\mathfrak{A}} [a | \emptyset'] : t'$ with $t' \leq_P t$.

**PROOF.** Straightforward structural induction on the derivation. □

**THEOREM 1.59 (SOUNDNESS).** If $\Gamma \vdash_{\mathfrak{A}} [\kappa | \mathfrak{k}] : t$, then $\Gamma \vdash [\kappa] : t$. If $\Gamma \vdash_{\mathfrak{A}} [a | \emptyset] : t$, then $\Gamma \vdash [a] : t$.

**PROOF.** We proceed by structural induction on the typing derivation of $\Gamma \vdash_{\mathfrak{A}} [\kappa | \mathfrak{k}] : t$ (resp. $\Gamma \vdash_{\mathfrak{A}} [a | \emptyset] : t$) in order to build a derivation $\Gamma \vdash [\kappa] : t$ (resp. $\Gamma \vdash [a] : t$). We consider the root of the derivation:

**[CONST-ALG]** Trivial (we use a `[CONST]` node).

**[Ax-ALG]** Trivial (we use a `[Ax_λ]` node).

**[→I-ALG]** We have $a \equiv \lambda x. \kappa$, and thus $\lfloor a \rfloor \equiv \lambda x. \lfloor \kappa \rfloor$.

By induction on the premise, we get $\Gamma, x : \mathfrak{u} \vdash [\kappa] : s$. By applying the rule `[→I]`, we get $\Gamma \vdash [a] : \mathfrak{u} \to s$ (with $t \approx \mathfrak{u} \to s$).

**[→E-ALG]** We have $a \equiv x_1 x_2$. We pose $t_1 \stackrel{\text{def}}{=} \Gamma(x_1)\Sigma_1$ and $t_2 \stackrel{\text{def}}{=} \Gamma(x_2)\Sigma_2$.

With an `[Ax_∀]` node, we can derive $\Gamma \vdash x_1 : \Gamma(x_1)$ and $\Gamma \vdash x_2 : \Gamma(x_2)$. Using a `[INST \wedge \le]` pattern, we can derive from that $\Gamma \vdash x_1 : t_1$ and $\Gamma \vdash x_2 : t_2$. We have $t \approx t_1 \circ t_2$. Thus, according to the definition of $\circ$, we know that $t_1 \le t_2 \to t$. Thus, with an application of the `[\le]` rule on $\Gamma \vdash x_1 : t_1$, we can derive $\Gamma \vdash x_1 : t_2 \to t$. We can then conclude with an application of the `[→E]` rule.

**[×I-ALG]** We have $a \equiv (x_1, x_2)$.

With an `[Ax_∀]` node, we can derive $\Gamma \vdash x_1 : \Gamma(x_1)\rho_1$ and $\Gamma \vdash x_2 : \Gamma(x_2)\rho_2$ (with $\rho_1$ and $\rho_2$ as in the `[×I-ALG]` node). We can then conclude with an application of the `[×I]` rule.

**[×E₁-ALG]** We have $a \equiv \pi_1 x$. We pose $t_o = \Gamma(x)\Sigma$.

With an `[Ax_∀]` node, we can derive $\Gamma \vdash x : \Gamma(x)$. Using a `[INST \wedge \le]` pattern, we can derive from that $\Gamma \vdash x : t_o$. We have $t \approx \pi_1(t_o)$. Thus, according to the definition of $\pi_1$, we know that $t_o \le t \times 1$. Thus, with an application of the `[\le]` rule, we can derive $\Gamma \vdash x : t \times 1$. We can then conclude with an application of the `[×E₁]` rule.

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

**[Ø-ALG]** Similar to the previous case.

**[ε₁-ALG]** Similar to the previous case.

**[ε₂-ALG]** Similar to the previous case.

**[Var-ALG]** Trivial (we use a `[Ax_∀]` node).

**[bind₁-ALG]** We have $\kappa \equiv \text{bind } x=a \text{ in } \kappa_o$ and thus $\lfloor \kappa \rfloor \equiv \lfloor \kappa_o \rfloor \{\lfloor a \rfloor / x\}$.

By induction on the premise, we get $\Gamma \vdash [\kappa_o] : t$. As $x \notin \text{dom}(\Gamma)$, we know that this derivation does not contain any `[Ax_∀]` node applied on $x$. We can thus easily transform it into a derivation of $\Gamma \vdash [\kappa_o] \{\lfloor a \rfloor / x\} : t$ by substituting every occurrence of $x$ by $\lfloor a \rfloor$.

**[bind₂-ALG]** We have $\kappa \equiv \text{bind } x=a \text{ in } \kappa_o$ and thus $\lfloor \kappa \rfloor \equiv \lfloor \kappa_o \rfloor \{\lfloor a \rfloor / x\}$.

We can suppose without loss of generality that the decomposition $\{\mathfrak{u}_i\}_{i \in I}$ is a partition of $1$: if for any two distinct $i, j \in I$, $\mathfrak{u}_i$ and $\mathfrak{u}_j$ are not disjoint, then we can replace the $\mathfrak{u}_j$ part by $\mathfrak{u}_j \setminus \mathfrak{u}_i$ and conclude by monotonicity (Lemma 1.58).

By induction on the first premise, we get $\Gamma \vdash [a] : s$. For any $i \in I$, we apply the induction hypothesis on the corresponding premise. It gives $\Gamma, x : s \wedge \mathfrak{u}_i \vdash [\kappa_o] : t_i$. With a `[\le]` node, we can obtain $\Gamma, x : s \wedge \mathfrak{u}_i \vdash [\kappa_o] : t$ (with $t \approx \bigvee_{i \in I} t_i$). We conclude with a `[\vee]` node.

**[∧-ALG]** Trivial induction on the premises. □
### 1.3.3 Completeness.

**DEFINITION 1.60 (ATOMIC SOURCE EXPRESSION).** We say that an expression of the source language is an atomic source expression if it can be constructed with the following syntax:

$$ \mathbf{Atomic~source~expressions} \quad \bar{a} ::= c \mid x \mid \lambda x.e \mid (x, x) \mid xx \mid \pi_i x \mid (x \in \tau) \ ? \ x : x $$

and if, for the case $\lambda x.e$, all sub-expressions of $e$ are either a binding variable or they contain a lambda variable that is not in $fv(\lambda x.e)$.

The variable $\bar{a}$ is used to range over atomic source expressions.

**DEFINITION 1.61.** For any atomic source expression $\bar{a}$, we define MSCA($\bar{a}$) as follows:

$$ \mathrm{MSCA}(\lambda x.e) = \lambda x.\mathrm{MSC}(e) $$

$$ \mathrm{MSCA}(\bar{a}) = \bar{a} \qquad \text{for any } \bar{a} \text{ that is not a } \lambda\text{-abstraction} $$

**PROPOSITION 1.62.** For any atomic source expression $\bar{a}$, $bind x = MSCA(\bar{a}) \ in \ x$ is a valid MSC-form.

**PROOF.** The extrusion property is ensured by the condition on $\lambda$-abstractions in Definition 1.60. The two other properties are trivially satisfied. $\square$

**DEFINITION 1.63.** For a binding context $B$ and an expression $e$, we define the operator $e \ \setminus \ B$ as follows:

$$ e \setminus \varepsilon = e $$

$$ e \setminus ((x, a); B) = (e\{x/\lceil a \rceil\}) \setminus B $$

**PROPOSITION 1.64.** For any binding context $B$ and expression $e$, we have $(e \ \setminus \ B)B \equiv_{\alpha} eB$ and $(eB) \ \setminus \ B \equiv_{\alpha} e \ \setminus \ B$.

**PROOF.** Straightforward induction on $B$. $\square$

In the following, we fix an expression order $\le$ over expressions (c.f. Desdefinition 1.9). This order should be total, so that for any expression $e$, it determines a unique MSC-form $\mathrm{MSC}(e)$ modulo $\alpha$-renaming (and not only modulo $\equiv_{\kappa}$): independent consecutive bindings must follow the increasing order $\le$ of their unwinding. As the order $\le$ is arbitrarily choosen, the proofs below will work for any MSC-form.

**LEMMA 1.65 (DECOMPOSITION OF CANONICAL FORM DERIVATIONS).** If $D$ is a canonical form derivation of $\Gamma \vdash e : t$, with the root being $a$ $[\vee]$ node doing the substitution $e'\{e_x/x\}$, then there exists a binding context $B$ such that $\mathrm{MSC}(e) \equiv_{\alpha} \mathrm{term}(B, bind x = \mathrm{MSCA}(e_x \setminus B) \text{ in } \mathrm{MSC}(e' \setminus B))$.

**PROOF.** First, we deduce from the fact that $D$ is a canonical form derivation that the definition premise, $\Gamma \vdash e_x : s$, is an atomic derivation.

We know that $e_x$ appears in $e$ (as $D$ is canonical, see Definition 1.7). Thus, we can deduce that $\mathrm{MSC}(e)$ contains a definition for an atom $a$ that unwinds to $e_x$. Formally, we know that there exists a binding context $B$, an atom $a$ and a canonical form $\kappa$ such that $\mathrm{MSC}(e) \equiv_{\alpha} \mathrm{term}(B, bind x = a \ in \ \kappa)$ with $\lceil a \rceil B \equiv_{\alpha} e_x$.

First, we determine what $B$ is. The expression $e_x$ could contain some sub-expressions that are not binding variables and that have no occurrence of a lambda variable defined in $e_x$. In this case, these sub-expressions should be defined by some bindings in $B$ (the unwinding of each such binding is necessarily smaller than $e_x$ by $\le$, as $\le$ is an extension of the sub-expressions order). The expression $e'$ could also contain some such sub-expressions. The ones whose unwnding is smaller than $e_x$ according to $\le$ must be defined by some bindings in $B$ too. No other expression should be defined in $B$ or it would contradict the properties of MSC-forms.
Now, we determine what *a* is. Under the context *B*, the expression *e*<sub>x</sub> \ *B* unwinds to *e*<sub>x</sub> (Proposition I.64). Moreover, as Γ ⊢ *e*<sub>x</sub> : *s* is an atomic derivation, and given how *B* is constructed, *e*<sub>x</sub> \ *B* must be an atomic source expression. Thus, we can deduce from Proposition I.62 that MSCA(*e*<sub>x</sub> \ *B*) can be used in place of the atom *a* without breaking any property of the MSC-form, and thus by unicity of the MSC-form (Proposition I.53) we can conclude that *a* ≡<sub>α</sub> MSCA(*e*<sub>x</sub> \ *B*).

Finally, we determine what *κ* is. We note *B'* the binding context *B*; (*x*, MSCA(*e*<sub>x</sub> \ *B*)). The expression *e'* \ *B'* unwinds to *e'*{*e*<sub>x</sub>/*x*} under the context *B'* (Proposition I.64). As *D* is a canonical form, *e*<sub>x</sub> cannot be a sub-expression of *e'* (c.f. Definition I.7), thus *e'* \ *B* ≡<sub>α</sub> *e'* \ *B'* and thus *e'* \ *B* also unwinds to *e'*{*e*<sub>x</sub>/*x*}. Thus, MSC(*e'* \ *B*) can be used in place of *κ* without breaking any property of the MSC-form (note that it only contains top-level bindings for expressions whose unwinding is greater than *e*<sub>x</sub> by ≤, as the smaller ones have been put in *B*). By unicity of the MSC-form (Proposition I.53), we conclude that *κ* ≡<sub>α</sub> MSC(*e'* \ *B*), and thus MSC(*e*) ≡<sub>α</sub> term(*B*, bind *x* = MSCA(*e*<sub>x</sub> \ *B*) in MSC(*e'* \ *B*)). □

Finally, we determine what $κ$ is. We note $B'$ the binding context $B$; $(x, \text{MSCA}(e_x \Bf B))$. The expression $e' \Bf B'$ unwinds to $e'[\{e_x/x\}]$ under the context $B'$ (Proposition I.64). As $D$ is a canonical form, $e_x$ cannot be a sub-expression of $e'$ (c.f. Definition I.7), thus $e' \Bf B \equiv_\alpha e' \Bf B'$ and thus $e' \Bf B$ also unwinds to $e'[\{e_x/x\}]$. Thus, MSC($e' \Bf B$) can be used in place of $κ$ without breaking any property of the MSC-form (note that it only contains top-level bindings for expressions whose unwinding is greater than $e_x$ by $≤$, as the smaller ones have been put in $B$). By unicity of the MSC-form (Proposition I.53), we conclude that $κ \equiv_\alpha \text{MSC}(e' \Bf B)$, and thus $\text{MSC}(e) \equiv_\alpha \text{term}(B, \text{bind } x = \text{MSCA}(e_x \Bf B) \text{ in } \text{MSC}(e' \Bf B))$. □

**LEMMA I.66 (COMPLETENESS).** If *D* is a canonical form derivation of Γ ⊢ *e* : *t*, then ∃k, *t'*. Γ ⊢<sub>Γ</sub>[MSC(*e*) | k] : *t'* with *t'* ≤*p* *t*.

If *D* is a canonical atomic derivation of Γ ⊢ ¯a : *t* (with ¯a an atomic source expression), then ∃ø, *t'*. Γ ⊢<sub>ø</sub>[MSCA(¯a) | ø] : *t'* with *t'* ≤*p* *t*.

**PROOF.** We proceed by induction on the depth of *D*.

We consider the root of the derivation (the cases up to [ε₂] are for canonical atomic derivations, the cases after are for canonical form derivations):

[CONST] Trivial.

[Ax_λ] Trivial.

[→I] We have ¯a ≡ λx. *e* and thus MSCA(¯a) ≡_α λx. MSC(*e*).

The premise of this [→I] node is a canonical form derivation. Thus, by induction on this premise, we get Γ, x : **u** ⊢<sub>Γ</sub> [MSC(*e*) | k] : *t'* (with *t'* ≤*p* *t*). We can thus derive Γ ⊢<sub>Γ</sub> [λx. MSC(*e*) | λ(**u**, k)] : **u** → *t'* and we have **u** → *t'* ≤*p* **u** → *t*, which concludes this case.

[→E] We have ¯a ≡ x₁x₂ and thus MSCA(¯a) ≡_α x₁x₂.

As *D* is a canonical atomic derivation, we know that the second premise, Γ ⊢ x₂ : t₁, is a [INST∧≤] pattern with no [≤] node and whose premise is a [Ax_⊕] node. Thus, we know that there exists Σ₂ such that Γ(x₂)Σ₂ ≈ t₁. Similarly, the first premise, Γ ⊢ x₁ : t₁ → t₂, is a [INST∧≤] pattern whose premise is a [Ax_⊕] node. Thus, we know that there exists Σ₁ such that Γ(x₁)Σ₁ ≤ t₁ → t₂.

Consequently, and by definition of ◦, we know that (Γ(x₁)Σ₁) ◦ (Γ(x₂)Σ₂) ≤ t₂. We can thus derive Γ ⊢<sub>Γ</sub> [x₁x₂ | @⟨Σ₁, Σ₂⟩] : *t'* (with *t'* ≈ (Γ(x₁)Σ₁) ◦ (Γ(x₂)Σ₂)) such that *t'* ≤ *t*₂, which concludes this case.

[×I] We have ¯a ≡ (x₁, x₂) and thus MSCA(¯a) ≡_α (x₁, x₂).

As *D* is a canonical atomic derivation, both premises can only be [Ax_⊕] nodes. Thus, we can deduce that there exists two renamings of polymorphic type variables ρ₁ and ρ₂ such that Γ(x₁)ρ₁ ≈ t₁ and Γ(x₂)ρ₂ ≈ t₂. Thus, we can derive Γ ⊢<sub>Γ</sub> [(x₁, x₂) | (ρ₁, ρ₂)] : t₁ × t₂.

[×E₁] We have ¯a ≡ π₁x and thus MSCA(¯a) ≡_α π₁x.

As *D* is a canonical atomic derivation, we know that the premise, Γ ⊢ x : t₁ × t₂, is a [INST∧≤] pattern whose premise is a [Ax_⊕] node. Thus, we know that there exists Σ such that Γ(x)Σ ≤ t₁ × t₂.

Consequently, and by definition of π₁, we know that π₁(Γ(x)Σ) ≤ t₁. We can thus derive Γ ⊢<sub>Γ</sub> [π₁x | π(Σ)] : *t'* (with *t'* ≈ π₁(Γ(x)Σ)) such that *t'* ≤ *t*₁, which concludes this case.

[×E₂] Similar to the previous case.
[0] We have $\bar{a} \equiv (x \in \tau) ? x_1 : x_2$ and thus MSCA($\bar{a}$) $\equiv_{\alpha}$ $(x \in \tau) ? x_1 : x_2$.

As D is a canonical atomic derivation, we know that the premise, $\Gamma \vdash x : \emptyset$, is a $[\text{INST} \wedge \le]$ pattern with no $\le$ node and whose premise is a $[\text{Ax}_\vee]$ node. Thus, we know that there exists $\Sigma$ such that $\Gamma(x)\Sigma \approx \emptyset$.

We can thus derive $\Gamma \vdash_{\mathcal{A}} [(x \in \tau) ? x_1 : x_2 | \emptyset(\Sigma)] : \emptyset$.

[$\epsilon_1$] We have $\bar{a} \equiv (x \in \tau) ? x_1 : x_2$ and thus MSCA($\bar{a}$) $\equiv_{\alpha}$ $(x \in \tau) ? x_1 : x_2$.

As D is a canonical atomic derivation, we know that the first premise, $\Gamma \vdash x : \tau$, is a $[\text{INST} \wedge \le]$ pattern whose premise is a $[\text{Ax}_\vee]$ node. Thus, we know that there exists $\Sigma$ such that $\Gamma(x)\Sigma \le \tau$. Similarly, the second premise, $\Gamma \vdash x_1 : t_1$, can only be a $[\text{Ax}_\vee]$. Thus, we know that there exists a renaming of polymorphic variables $\rho$ such that $\Gamma(x_1)\rho \approx t_1$.

We can thus derive $\Gamma \vdash_{\mathcal{A}} [(x \in \tau) ? x_1 : x_2 | \epsilon_1(\Sigma)] : \Gamma(x_1)$ with $\Gamma(x_1) \leq_P t_1$.

[$\epsilon_2$] Similar to the previous case.

$[\mathbf{Ax}_\vee]$ Trivial.

$\leq$ Straightforward induction on the premise.

$[\text{INST}]$ Straightforward induction on the premise.

[A] By induction on the premises, we get $\forall i \in I$. $\Gamma \vdash_{\mathcal{A}} [\text{MSC}(e) | \mathcal{K}_i] : t'_i$ with $t'_i \le_P t_i$. Thus, we can derive $\Gamma \vdash_{\mathcal{A}} [\text{MSC}(e) | \bigwedge(\{\mathcal{K}_i\}_{i \in I})] : \bigwedge_{i \in I} t'_i$ (with $\bigwedge_{i \in I} t'_i \le_P \bigwedge_{i \in I} t_i$).

[V] By using Lemma 1.65, we know that there exists B such that MSC(e) $\equiv_{\alpha}$ B[$\text{bind } x = \text{MSC}(e_x \setminus B)$ in MSC(e' \ B)] (with $e_x \setminus B$ being an atomic source expression).

The unwiding of the top-level definitions in B are necessarily smaller than $e_x$ by $\le$. Thus, none of them can be defined by a $[\vee]$ node in D. Consequently, and as in canonical form derivation a structural node can only appear in the first premise of a $[\vee]$ node, none of the expressions defined in B are typed in D. Thus, these sub-expressions can easily be substituted, in D, by the associated binding variables in B. It yields a derivation for $\Gamma \vdash (e'\{e_x/x\}) \setminus B : t$, or equivalently, for $\Gamma \vdash (e' \setminus B)\{(e_x \setminus B)/x\} : t$.

By induction on the premises of this new derivation, we get $\Gamma \vdash_{\mathcal{A}} [\text{MSC}(e_x \setminus B) | \emptyset] : s'$ (with $s' \le_P s$) and $\forall i \in I$. $\Gamma, x : s \wedge \mathbf{u}_i \vdash_{\mathcal{A}} [\text{MSC}(e' \setminus B) | \mathcal{K}_i] : t_i$ (with $t_i \le_P t$). By monotonicity (Lemma 1.58), we can derive $\forall i \in I$. $\Gamma, x : s' \wedge \mathbf{u}_i \vdash_{\mathcal{A}} [\text{MSC}(e' \setminus B) | \mathcal{K}'_i] : t'_i$ (with $t'_i \le_P t_i \le_P t$). We can thus derive $\Gamma \vdash_{\mathcal{A}} [\text{bind } x = \text{MSC}(e_x \setminus B) \text{ in } \text{MSC}(e' \setminus B) | \mathcal{K}] : \bigvee_{i \in I} t'_i$ with $\mathcal{K} = \text{keep } (\emptyset, \{(\mathbf{u}_i, \mathcal{K}'_i)\}_{i \in I})$.

From that, we can easily derive $\Gamma \vdash_{\mathcal{A}} [\text{MSC}(e) | \mathcal{K}] : \bigvee_{i \in I} t'_i$ with $\mathcal{K}'$ obtained by inserting at the root of $\mathcal{K}$ a skip annotation for each definition in B.

□

**THEOREM 1.67 (COMPLETENESS).** If $\Gamma \vdash e : t$ with $e$ a ground expression, then $\exists \mathcal{K}, t' : \Gamma \vdash_{\mathcal{A}} [\text{MSC}(e) | \mathcal{K}] : t'$ with $t' \le_P t$.

**PROOF.** Direct application of Lemma 1.66 after using the normalisation theorem (Theorem 1.22) on a derivation of $\Gamma \vdash e : t$. □

## I.4 Annotations Reconstruction System

This section contains proofs for the reconstruction system (Appendix H).

**THEOREM I.68 (SOUNDNESS).** If $\Gamma \vdash \langle \kappa | \mathcal{K} \rangle \Rightarrow \mathcal{K}$, then $\exists t. \Gamma \vdash_{\mathcal{A}} [\kappa | \mathcal{K}] : t$. If $\Gamma \vdash_{\mathcal{P}} \langle a | \mathcal{A} \rangle \Rightarrow \emptyset$, then $\exists t. \Gamma \vdash_{\mathcal{A}} [a | \emptyset] : t$.

**PROOF.** We proceed by structural induction on the derivation of $\Gamma \vdash_{\mathcal{P}} \langle \kappa | \mathcal{K} \rangle \Rightarrow \mathcal{K}$ or $\Gamma \vdash_{\mathcal{P}} \langle a | \mathcal{A} \rangle \Rightarrow \emptyset$.

If the derivation $\Gamma \vdash_{\mathcal{P}} \langle a | \mathcal{A} \rangle \Rightarrow \emptyset$ has a $[\text{APP}]$ root, we construct a derivation $\Gamma \vdash_{\mathcal{A}} [a | \emptyset] : t$ (for some $t$) with a $[\rightarrow \text{E-ALG}]$ root. In order to satisfy the guard-conditions of the rule $[\rightarrow \text{E-ALG}]$, we
need to prove that the annotation @($\Sigma_1$, $\Sigma_2$) generated by the [App] root satisfies $\Gamma(x_1)\Sigma_1 \le \emptyset \to 1$ and $\Gamma(x_2)\Sigma_2 \le \text{dom}(\Gamma(x_1)\Sigma_1)$.

We have, in the premise of the [App] root, $\Sigma = \text{tally}(\{\Gamma(x_1)\rho_1 \le \Gamma(x_2)\rho_2 \to \alpha\})$ and $\Sigma \ne \emptyset$. Let $\sigma \in \Sigma$. By definition of the tallying problem, we have $(\Gamma(x_1)\rho_1)\sigma \le (\Gamma(x_2)\rho_2 \to \alpha)\sigma$, which can be rewritten $\Gamma(x_1)(\sigma \circ \rho_1) \le (\Gamma(x_2)(\sigma \circ \rho_2)) \to (\alpha\sigma)$. From that subtyping relation, we can deduce $\Gamma(x_1)(\sigma \circ \rho_1) \le \emptyset \to 1$, and by definition of $\text{dom}(.)$, $\Gamma(x_2)(\sigma \circ \rho_2) \le \text{dom}(\Gamma(x_1)(\sigma \circ \rho_1))$. As $(\sigma \circ \rho_2) \in \Sigma_2$ and $(\sigma \circ \rho_1) \in \Sigma_1$, we deduce $\Gamma(x_1)\Sigma_1 \le \emptyset \to 1$ and $\Gamma(x_2)\Sigma_2 \le \text{dom}(\Gamma(x_1)\Sigma_1)$ (we use the fact that $\text{dom}(.)$ is monotonically non-increasing).

The other cases are similar or straightforward. □

Now, we propose a sketch of proof justifying that the deduction rules for the reconstruction system define a terminating algorithm. The idea of this proof is similar to the proof of termination of the *Kirby-Paris hydra game*<fnref n="12" />: we can associate an ordinal number weight to each node, and this weight can only decrease as the game (or derivation) advances. Intuitively, this non-negative weight represents the advancement of the game (or derivation). Though sub-trees can sometimes be duplicated, their weight is always lowered before being duplicated, resulting in a lower weight overall.

For any type environment $\Gamma$, canonical form or atom $\eta$, and intermediate annotation $\mathcal{H}$ compatible with the structure of $\eta$, the weight $w(\Gamma, \eta, \mathcal{H})$ is the ordinal number defined as follows:

$$w(\Gamma, \eta, \text{typ}) = 1$$

$$w(\Gamma, \eta, \text{untyp}) = 1$$

$$w(\Gamma, \eta, \wedge(S_1, S_2)) = \sum\{w(\Gamma, \eta, \mathcal{H}) \mid \mathcal{H} \in S_1\}$$

$$w(\Gamma, c, \text{infer}) = \omega$$

$$w(\Gamma, \lambda x.\kappa, \text{infer}) = \omega^{w(\Gamma, \kappa, \text{infer})}$$

$$w(\Gamma, x, \text{infer}) = \omega$$

$$w(\Gamma, \lambda x.\kappa, \lambda(u, \mathcal{K})) = \omega^{w(\Gamma, \kappa, \mathcal{K})}$$

$$w(\Gamma, \pi_i x, \text{infer}) = \omega$$

if $x \in \text{dom}(\Gamma)$

$$w(\Gamma, \pi_i x, \text{infer}) = \omega^2$$

otherwise

$$w(\Gamma, x_1 x_2, \text{infer}) = \omega$$

if $\{x_1, x_2\} \subseteq \text{dom}(\Gamma)$

$$w(\Gamma, x_1 x_2, \text{infer}) = \omega^2$$

otherwise, if $x_1 \in \text{dom}(\Gamma)$

$$w(\Gamma, x_1 x_2, \text{infer}) = \omega^2$$

otherwise, if $x_2 \in \text{dom}(\Gamma)$

$$w(\Gamma, x_1 x_2, \text{infer}) = \omega^3$$

otherwise

$$w(\Gamma, (x_1, x_2), \text{infer}) = \omega$$

if $\{x_1, x_2\} \subseteq \text{dom}(\Gamma)$

$$w(\Gamma, (x_1, x_2), \text{infer}) = \omega^2$$

otherwise, if $x_1 \in \text{dom}(\Gamma)$

$$w(\Gamma, (x_1, x_2), \text{infer}) = \omega^2$$

otherwise, if $x_2 \in \text{dom}(\Gamma)$

$$w(\Gamma, (x_1, x_2), \text{infer}) = \omega^3$$

otherwise

<footnote n="12">¹²https://en.wikipedia.org/wiki/Hydra game</footnote>
$$w(\Gamma, (x_0 \in \tau) ? x_1 : x_2, \epsilon_i) = \omega$$

$$w(\Gamma, (x_0 \in \tau) ? x_1 : x_2, \inferr{\text{infer}}) = \omega^2$$

$$\text{if } \Gamma(x_0) \leq \tau$$

$$w(\Gamma, (x_0 \in \tau) ? x_1 : x_2, \inferr{\text{infer}}) = \omega^2$$

$$\text{otherwise, if } \Gamma(x_0) \leq \neg \tau$$

$$w(\Gamma, (x_0 \in \tau) ? x_1 : x_2, \inferr{\text{infer}}) = \omega^3$$

$$\text{otherwise, if } x_0 \in \text{dom}(\Gamma)$$

$$w(\Gamma, (x_0 \in \tau) ? x_1 : x_2, \inferr{\text{infer}}) = \omega^4$$

$$\text{otherwise}$$

$$w(\Gamma, \text{bind } x = a \text{ in } \kappa, \text{skip } (\mathcal{K})) = \omega^{w(\Gamma, \kappa, \mathcal{K})}$$

$$w(\Gamma, \text{bind } x = a \text{ in } \kappa, \text{keep } (\mathcal{A}, S_1, S_2)) = \omega^{\alpha}$$

$$\text{with } \alpha = \sum \{w((\Gamma, x : \mathbf{u}), \kappa, \mathcal{K}) \mid (\mathbf{u}, \mathcal{K}) \in S_1\}$$

$$w(\Gamma, \text{bind } x = a \text{ in } \kappa, \text{propagate } (\mathcal{A}, \Gamma, S_1, S_2)) = \omega^{\alpha+|\Gamma|}$$

$$\text{with } \alpha = \sum \{w((\Gamma, x : \mathbf{u}), \kappa, \mathcal{K}) \mid (\mathbf{u}, \mathcal{K}) \in S_1\}$$

$$w(\Gamma, \text{bind } x = a \text{ in } \kappa, \text{try-keep } (\mathcal{A}, \mathcal{K}_1, \mathcal{K}_2)) = \omega^{\alpha}$$

$$\text{with } \alpha = \sum \{w(\Gamma, a, \mathcal{A}), w((\Gamma, x : \mathbf{1}), \kappa, \mathcal{K}_1), w(\Gamma, \kappa, \mathcal{K}_2)\}$$

$$w(\Gamma, \text{bind } x = a \text{ in } \kappa, \text{try-skip } (\mathcal{K})) = \omega^{\alpha}$$

$$\text{with } \alpha = \sum \{w(\Gamma, a, \inferr{\text{infer}}), w(\Gamma, \kappa, \mathcal{K})\}$$

$$w(\Gamma, x, \inferr{\text{infer}}) = \omega$$

$$\text{if } x \in \text{dom}(\Gamma)$$

$$w(\Gamma, x, \inferr{\text{infer}}) = \omega^2$$

$$\text{otherwise}$$

where, for any multiset $\{\alpha_1, \alpha_2, \dots, \alpha_n\}$, $\sum \{\alpha_1, \alpha_2, \dots, \alpha_n\} \stackrel{\text{def}}{=} \alpha_1 + \alpha_2 + \dots + \alpha_n$ with $\alpha_1 \ge \alpha_2 \ge \dots \ge \alpha_n$.

Then, we define a weight $w(\Gamma, \eta, \mathbb{R})$ for any type environment $\Gamma$, canonical form or atom $\eta$, and result $\mathbb{R}$ compatible with the structure of $\eta$:

$$w(\Gamma, \eta, \text{Ok}(\mathcal{H})) = 1$$

$$w(\Gamma, \eta, \text{Fail}) = 1$$

$$w(\Gamma, \eta, \text{Split}(\Gamma', \mathcal{H}_1, \mathcal{H}_2)) = \sum \{w(\Gamma \wedge \Gamma', \eta, \mathcal{H}_1)\} \cup \{w((\Gamma, x : \neg \mathbf{u}), \eta, \mathcal{H}_2) \mid (x : \mathbf{u}) \in \Gamma'\}$$

$$w(\Gamma, \eta, \text{Subst}(\{\psi_i\}_{i \in I}, \mathcal{H}_1, \mathcal{H}_2)) = \sum \{w(\Gamma, \eta, \mathcal{H}_2)\} \cup \{w(\Gamma, \psi_i, \eta, \mathcal{H}_1 \psi_i) \mid i \in I\}$$

$$w(\Gamma, \eta, \text{Var}(x, \mathcal{H}_1, \mathcal{H}_2)) = \sum \{w((\Gamma, x : \mathbf{1}), \eta, \mathcal{H}_1), w(\Gamma, \eta, \mathcal{H}_2)\}$$

**LEMMA I.69.** For any $\Gamma, \eta, \mathcal{H}$, and $\Gamma'$ such that $\Gamma' \le \Gamma$, we have $w(\Gamma', \eta, \mathcal{H}) \le w(\Gamma, \eta, \mathcal{H})$.

**PROOF.** Straightforward induction.

☐

**LEMMA I.70.** For any $\Gamma, \eta, \mathcal{H}$, and $\psi$, we have $w(\Gamma\psi, \eta, \mathcal{H}\psi) \le w(\Gamma, \eta, \mathcal{H})$.

**PROOF.** Straightforward induction (we recall that test types $\tau$ do not contain type variables).

☐

**LEMMA I.71.** If $\Gamma \vdash_R \langle\eta | \mathcal{H}\rangle \Rightarrow \mathbb{R}$ or $\Gamma \vdash_R^* \langle\eta | \mathcal{H}\rangle \Rightarrow \mathbb{R}$, then $w(\Gamma, \eta, \mathcal{H}) \ge w(\Gamma, \eta, \mathbb{R})$.

**PROOF.** Structural induction on the derivation of $\Gamma \vdash_R \langle\eta | \mathcal{H}\rangle \Rightarrow \mathbb{R}$ or $\Gamma \vdash_R^* \langle\eta | \mathcal{H}\rangle \Rightarrow \mathbb{R}$.

☐

**THEOREM I.72 (TERMINATION).** The deduction rules $\vdash_R^*$ and $\vdash_R$ define a terminating algorithm: it can either fail (if no rule applies at some point) or return a result $\mathbb{R}$.

**PROOF.** There can only be finitely many $[\text{ITERATE}_1]$ and $[\text{ITERATE}_2]$ nodes applied on a given canonical form or atom, otherwise, according to the previous lemmas, we could extract from them an infinite decreasing chain of ordinal numbers.

☐
Received 2023-07-11; accepted 2023-11-07