Typed Intermediate Languages and Certified Closure Conversion

Proof. Strengthen the statement to the form the induction actually needs: if $\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{F}e:\tau$ and $\mathrm{\Delta };[[\mathrm{\Gamma }{]]}_K{⊢}_{K}k:\mathsf{Cont}[[\tau {]]}_K$, then $\mathrm{\Delta };[[\mathrm{\Gamma }{]]}_K{⊢}_K[[e{]]}_{K}k$. The unstrengthened statement is not an induction hypothesis, because the translation of a subterm is applied to a continuation built by the translation of its context.

Induct on the ${\lambda }^F$ typing derivation. Variable and integer. $[[x^{\tau }{]]}_{K}k=k(x)$, and the call rule of ${\lambda }^K$ applies because $k$ has type $\mathsf{Cont}[[\tau {]]}_K$ and $x$ has type $[[\tau {]]}_K$ in $[[\mathrm{\Gamma }{]]}_K$.

Application. Let $\mathrm{\Delta };\mathrm{\Gamma }{⊢}_F{u}_1:{\tau }_1\to {\tau }_2$ and $\mathrm{\Delta };\mathrm{\Gamma }{⊢}_F{u}_2:{\tau }_1$. The inner continuation $\lambda x_2:[[{\tau }_1{]]}_K.x_1(x_2,k)$ is well typed in $[[\mathrm{\Gamma }{]]}_K,x_1:[[{\tau }_1\to {\tau }_2{]]}_K$, because $[[{\tau }_1\to {\tau }_2{]]}_K=([[{\tau }_1{]]}_K,\mathsf{Cont}[[{\tau }_2{]]}_K)\to \mathsf{void}$ is exactly the type of a function taking the argument and the continuation. It therefore has type $\mathsf{Cont}[[{\tau }_1{]]}_K$, which is what the induction hypothesis for $u_2$ requires. The outer continuation is then well typed at $\mathsf{Cont}[[{\tau }_1\to {\tau }_2{]]}_K$, which is what the induction hypothesis for $u_1$ requires.

Recursive function. Its translation is the call $$k(\mathsf{fix}x(x_1:[[{\tau }_1{]]}_K,c:\mathsf{Cont}[[{\tau }_2{]]}_K).[[e{]]}_{K}c).$$ Applying the induction hypothesis to the body with the continuation variable $c$ gives the body’s well-formedness; the ${\lambda }^K$ function rule then types the value at $[[{\tau }_1\to {\tau }_2{]]}_K$, and the call rule applies $k$ to it.

Type abstraction and application, tuples, projection, arithmetic and $\mathsf{if}\mathsf{0}$ follow the same two moves: build the continuation demanded by the induction hypothesis of each subterm, and apply the ${\lambda }^K$ rule whose premises the hypotheses supply. The $\mathsf{if}\mathsf{0}$ case is the only one that uses $k$ twice; both uses are at the same type, so no duplication of typing obligations arises. Finally, $\lambda x:[[\tau {]]}_K.\mathsf{halt}[[[\tau {]]}_K]x$ has type $\mathsf{Cont}[[\tau {]]}_K$, which discharges the strengthened statement at the top level. ◻

Proof. Induct on the ${\lambda }^K$ derivation, with the invariant that a ${\lambda }^K$ value of type $\tau$ becomes a ${\lambda }^C$ value of type $[[\tau {]]}_C$ and a well-formed term becomes a well-formed term.

The one case that is not a rewriting is $\mathsf{fix}$. Let the free term variables of the ${\lambda }^K$ function be $y_1:{\sigma }_1,\dots ,y_m:{\sigma }_m$ and its free type variables be $\overrightarrow{\gamma }$. Build the environment value $v_{\mathrm{env}}=⟨y_1,\dots ,y_m⟩$ of type ${\sigma }_{\mathrm{env}}=⟨[[{\sigma }_1{]]}_C,\dots ,[[{\sigma }_m{]]}_C⟩$, and the code block $$v_{\mathrm{code}}=\mathsf{fix}x[\overrightarrow{\gamma },\overrightarrow{\alpha }](z:{\sigma }_{\mathrm{env}},x_1:[[{\tau }_1{]]}_C,\dots ).\mathsf{let}⟨y_1,\dots ,y_m⟩=z\mathsf{in}[[e{]]}_C,$$ whose body has no free term variable other than those bound by the block, so C-Fix applies with the context $\overrightarrow{\gamma },\overrightarrow{\alpha }$. The closure is $$\mathsf{pack}[{\sigma }_{\mathrm{env}},⟨v_{\mathrm{code}}[\overrightarrow{\gamma }],v_{\mathrm{env}}⟩]\mathsf{as}[[\tau {]]}_C.$$ C-TApp types $v_{\mathrm{code}}[\overrightarrow{\gamma }]$ — this is where partial type application being a value does the work — and C-Pack then hides ${\sigma }_{\mathrm{env}}$. At a call site, C-Unpack and two projections recover the code at type $\mathrm{\forall }[\overrightarrow{\alpha }](\beta ,\dots )\to \mathsf{void}$ and the environment at type $\beta$, for the freshly bound $\beta$; the call rule then applies.

The remaining cases replace each subterm by its translation and reapply the same rule; no type changes shape except through construction 133.6, and that shape is exactly what the call case consumes. ◻

Proof. After lemma 133.7 every code block is closed, so moving it to the top level changes no free variable. Formally, induct on $e$, carrying a heap typing $\mathrm{\Psi }$ that assigns to each fresh label the type its block had as a value; each C-Fix node contributes one binding, and the label is typed by the heap rule at exactly that type. ◻

Proof. Induct on the ${\lambda }^H$ derivation. The tuple case is the only one whose translation is not a renaming: it emits the sequence of example 133.10, and after the $n$th update the bound variable has the type $⟨[[{\tau }_1{]]}_A^1,\dots ,[[{\tau }_n{]]}_A^1⟩$, which is $[[⟨{\tau }_1,\dots ,{\tau }_n⟩{]]}_A$. Every subsequent projection therefore satisfies the side condition of A-Proj. Because a ${\lambda }^H$ value may itself contain a tuple, the value translation returns a sequence of declarations together with a value; the induction hypothesis is stated for that pair, and the declaration sequences are concatenated in the order the subterms are traversed. ◻

Proof. Both halves are structural inductions over the instruction at the head of $I$, and both rest on the same three auxiliary facts. Canonical word forms: if ${⊢}_{\mathrm{TAL}}H:\mathrm{\Psi }$ and $\mathrm{\Psi };\varnothing {⊢}_{\mathrm{TAL}}w:\tau \mathsf{wval}$, then the shape of $w$ is determined by the outermost constructor of $\tau$ — an integer for $\mathsf{int}$, a label for a tuple or code type, a package for an existential. Heap extension and update: adding a label at a type not already in $\mathrm{\Psi }$, or overwriting a field with a value of a subtype of its recorded type, preserves ${⊢}_{\mathrm{TAL}}H:\mathrm{\Psi }$. Register file update: writing a well-typed word into $r_d$ preserves $\mathrm{\Psi }{⊢}_{\mathrm{TAL}}R:\mathrm{\Gamma }$ at the updated $\mathrm{\Gamma }$.

For progress at $\mathsf{jmp}v$: typing gives $\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{\mathrm{TAL}}v:\mathrm{\forall }[].{\mathrm{\Gamma }}^{\prime }$ and ; canonical word forms make $\hat{R}(v)$ a label instantiation $\ell [\overrightarrow{\tau }]$, the heap typing supplies a code block at $\ell$, and the machine rule applies. For subject reduction at the same instruction, the substituted instruction sequence is well typed because code block typing is closed under type substitution and lets the register file be weakened to the block’s assumptions. At $\mathsf{ld}{r}_d,r_s[i]$, canonical forms give $R(r_s)=\ell$ with $H(\ell )=⟨w_0,\dots ,w_{n-1}⟩$; the initialization flag carried into TAL from ${\lambda }^A$ is what guarantees and that $w_i$ is a well-typed word rather than a junk value $?\tau$. At $\mathsf{malloc}{r}_d[\overrightarrow{\tau }]$ the fresh label is added with all fields junk and all flags $0$, which is exactly the case heap extension covers. The remaining instructions are register-to-register moves and arithmetic and are handled by register file update alone. ◻

Proof. Compose lemma 133.4, lemma 133.7, lemma 133.8, lemma 133.11, lemma 133.15, each of whose conclusion is the hypothesis of the next. ◻

Proof. Let $\mathcal{Z}(e)=(\varnothing ,\{r_1\mapsto 0\},\mathsf{halt}[\mathsf{int}])$ for every $e$. The heap typing is empty, the register file typing is $\{r_1:\mathsf{int}\}$, and $\mathsf{halt}[\mathsf{int}]$ requires exactly that, so ${⊢}_{\mathrm{TAL}}\mathcal{Z}(e)$ for every $e$. Taking $e=e_{\mathrm{fact}}$ gives the stated behaviours. ◻

Proof. The heap typing rule checks each heap value against $\mathrm{\Psi }$. Every such check in $H_1$ used only labels in ${\mathrm{\Psi }}_1$ or imported labels, and heap value typing is monotone in $\mathrm{\Psi }$ by the heap extension lemma of theorem 133.13; the imported labels are present in ${\mathrm{\Psi }}_1\uplus {\mathrm{\Psi }}_2$ at the assumed types. Disjointness of domains makes the union a function. ◻