Chapter 134Optional

A Certified Type-Preserving Compiler to Assembly

Prerequisites. Direct starred prerequisites: Chapter 133 and chapter 31. No later core chapter depends on this route.

The pipeline of chapter 133 maps a well-typed source program to a well-typed assembly program and says nothing about what either computes. To say something about what they compute, three things are needed that the previous chapter did not have: a semantics for the source language, a semantics for the assembly language, and a relation between them that survives five intermediate languages.

The first is easy and the third is the subject of this chapter. The second is where the difficulty starts. A source term of type $Nat$ denotes a natural number. An assembly program denotes — what? It may diverge, so it does not denote a number. It reads and writes an untyped heap of machine words, so its meaning depends on a heap whose contents the type system has stopped describing. And it calls a runtime system that may move every object in that heap between two instructions. A semantics that is silent about any of these cannot support a preservation theorem, and a semantics that models all of them in the wrong way makes the theorem unprovable.

This chapter reconstructs Chlipala’s certified compiler (2007): six type-directed translations from the simply typed lambda calculus to an idealized assembly language, each with a denotational semantics and a machine-checked semantics-preservation proof, composed into one correctness theorem.

Syntax that is a typing derivation

Definition 134.1 — Intrinsically typed source syntax ¶

Source types and terms are the indexed families $\begin{aligned} sty & : Set, & SNat & : sty, & SArrow & : sty \to sty \to sty, \\ sterm & : list sty \to sty \to Set, \end{aligned}$ with constructors $\begin{aligned} SVar & : Π Γ, Π t . var Γ t \to sterm Γ t, \\ SLam & : Π Γ, Π d, Π r . sterm (d :: Γ) r \to sterm Γ (SArrow d r), \\ SApp & : Π Γ, Π d, Π r . sterm Γ (SArrow d r) \to sterm Γ d \to sterm Γ r, \\ SConst & : Π Γ . N \to sterm Γ SNat, \end{aligned}$ where $var Γ t$ is the family of de Bruijn indices witnessing that $t$ occurs in $Γ$ : it has $First : Π Γ, Π t . var (t :: Γ) t$ and $Next : Π Γ, Π t, Π t^{'} . var Γ t \to var (t^{'} :: Γ) t$ .

Referenced from 5 locations

A Certified Type-Preserving Compiler to Assembly

An element of $sterm Γ t$ is not a raw tree that a separate judgment later accepts. It is the typing derivation: there is no constructor producing an ill-typed term, and there is no typing judgment to state. That single decision determines the shape of every theorem below.

Proposition 134.2 — Type preservation has no content here ¶

Let $L_{1}$ and $L_{2}$ be languages presented as in definition 134.1, and let $T : Π Γ, Π t . L_{1} Γ t \to L_{2} (F Γ) (F t)$ be a total function of the metatheory, for some type translation $F$ . Then $T$ preserves typing.

Referenced from 6 locations

Proof of Proposition 134.2 — Type preservation has no content here

Proof. “ $T$ preserves typing” says: for every $Γ$ , $t$ and $e \in L_{1} Γ t$ , the output lies in $L_{2} (F Γ) (F t)$ . That is the codomain of $T$ . A function inhabits its stated type, so the statement is discharged by the fact that $T$ is well typed. ◻

This is not a trick. It relocates work rather than removing it: the type preservation lemmas of chapter 133 become obligations discharged while writing each translation, and what remains to be proved is the part those lemmas never touched — that the translation preserves meaning. Section 134.3 shows the price.

Definition 134.3 — Denotation of the source language ¶

Interpret types and contexts by $[[SNat]] = N, [[SArrow t_{1} t_{2}]] = [[t_{1}]] \to [[t_{2}]], [[Γ]] = [[t_{1}]] \times \dots \times [[t_{n}]],$ and a term $e \in sterm Γ t$ by a function $[[e]] : [[Γ]] \to [[t]]$ : $\begin{aligned} [[SVar v]] σ & = σ (v), & [[SConst n]] σ & = n, \\ [[SLam e^{'}]] σ & = λ x . [[e^{'}]] (x, σ), & [[SApp e_{1} e_{2}]] σ & = ([[e_{1}]] σ) ([[e_{2}]] σ) . \end{aligned}$

Referenced from 2 locations

A Certified Type-Preserving Compiler to Assembly

The object language’s binder is interpreted by the metalanguage’s binder. This is what makes the semantics usable in a proof assistant: no environment manipulation, no substitution lemma, and — as section 134.5 shows — no need to say what a closure is.

Linearization and its composition operator

Definition 134.4 — Linear ¶

$o ::= n ∣ x ∣ λ x : τ . e, e ::= let x = o in e ∣ throw ⟨ o ⟩ ∣ x y z .$ A Linear term is a sequence of bindings of primitive operands, ending either in a throw to the current continuation or in a function call; a function takes its ordinary argument and its continuation. Its denotation takes a substitution and a continuation: $[[e]] : [[Γ]] \to ([[τ]] \to R) \to R$ .

Referenced from 4 locations

A Certified Type-Preserving Compiler to Assembly

Definition 134.5 — Splicing ¶

For Linear terms $e_{1}$ in $Γ$ and $e_{2}$ in $τ :: Γ$ , the term $e_{1} ∙^{u} e_{2}$ runs $e_{1}$ and binds its result to $u$ in $e_{2}$ : $\begin{aligned} (let y = o in e_{1}) ∙^{u} e_{2} & = let y = o in (e_{1} ∙^{u} e_{2}), \\ (throw ⟨ o ⟩) ∙^{u} e_{2} & = let u = o in e_{2}, \\ (x y z) ∙^{u} e_{2} & = let f = (λ v . let g = (λ u . e_{2}) in z v g) in x y f . \end{aligned}$ Linearization is then $\begin{aligned} [[n {]]}_{L} & = throw ⟨ n ⟩, & [[x {]]}_{L} & = throw ⟨ x ⟩, \\ [[λ x : τ . e {]]}_{L} & = throw ⟨ λ x : τ . [[e {]]}_{L} ⟩, \end{aligned}$ and, for an application, $[[e_{1} e_{2} {]]}_{L} = [[e_{1} {]]}_{L} ∙^{u} ([[e_{2} {]]}_{L} ∙^{v} (let f = (λ x . throw ⟨ x ⟩) in u v f)) .$

Referenced from 6 locations

A Certified Type-Preserving Compiler to Assembly

Lemma 134.6 — Splicing is sound ¶

For all $Γ$ , $t$ , $e \in lterm Γ t$ , $t^{'}$ , $e^{'} \in lterm (t :: Γ) t^{'}$ , every substitution $σ$ and every continuation $k$ , $[[e ∙^{u} e^{'}]] σ k = [[e]] σ (λ x . [[e^{'}]] (x, σ) k) .$

Referenced from 5 locations

A Certified Type-Preserving Compiler to Assembly

Proof of Lemma 134.6 — Splicing is sound

Proof. Induction on $e$ . Throw. Both sides reduce to $[[e^{'}]] ([[o]] σ, σ) k$ : the left by unfolding the $let$ clause of the Linear denotation on $let u = o in e^{'}$ , the right by unfolding the throw clause $[[throw ⟨ o ⟩]] σ k^{'} = k^{'} ([[o]] σ)$ and applying the displayed $k^{'}$ .

Let. With $e = let y = o in e_{1}$ , unfolding the $let$ clause on both sides leaves $[[e_{1} ∙^{u} e^{'}]] ([[o]] σ, σ) k$ on the left and $[[e_{1}]] ([[o]] σ, σ) (λ x . [[e^{'}]] (x, σ) k)$ on the right — except that $e^{'}$ is now used under one more binder, so the right-hand side is really $[[e^{'}]] (x, ([[o]] σ, σ)) k$ . The induction hypothesis closes the case exactly when the two readings agree, which is lemma 134.8 below.

Call. With $e = x y z$ , the left side unfolds the two $let$ -bound abstractions and then the call clause $[[x y z]] σ k = σ (x) σ (y) σ (z)$ , giving $σ (x) σ (y) (λ v . σ (z) v (λ u . [[e^{'}]] (u, σ) k))$ . The right side is $σ (x) σ (y) σ (z)$ applied to $λ x . [[e^{'}]] (x, σ) k$ ; the two agree because the metalanguage function $σ (z)$ is applied to the same two arguments in both. ◻

Theorem 134.7 — Linearization is sound ¶

For every $Γ$ , $t$ and $e \in sterm Γ t$ , every $σ$ and every $k$ , $[[[[e {]]}_{L}]] σ k = k ([[e]] σ)$ .

Referenced from 4 locations

A Certified Type-Preserving Compiler to Assembly

Proof of Theorem 134.7 — Linearization is sound

Proof. Induction on $e$ . Constant and variable unfold the throw clause directly. Abstraction unfolds the throw clause and then the induction hypothesis at the body, under the metalanguage binder. Application applies lemma 134.6 twice, then the two induction hypotheses, then the call clause; the residual continuation $λ x . throw ⟨ x ⟩$ denotes the identity, which is what leaves $k$ applied to $([[e_{1}]] σ) ([[e_{2}]] σ)$ . ◻

The price of intrinsic typing

In the application clause of definition 134.5, the subterm $[[e_{2} {]]}_{L}$ was built in $Γ$ and is used in $u : τ_{1} :: Γ$ . Mathematically this is harmless. With intrinsic syntax it is a type error: the term inhabits $lterm Γ t$ and the position demands $lterm (τ_{1} :: Γ) t$ . A coercion is required, and the coercion is a function that renumbers de Bruijn indices: $weakenFront : Π Γ, Π τ . lterm Γ τ \to Π τ^{'} . lterm (τ^{'} :: Γ) τ .$ This function is the weakening lemma “if $Γ ⊢ e : τ$ then $Γ, x : τ^{'} ⊢ e : τ$ when $x$ is not free in $e$ ”, written as a program. Since it is a program and not a lemma, it must be accompanied by the lemma that it does not change meaning.

Lemma 134.8 — Weakening is denotation-preserving ¶

For every $e \in lterm Γ τ$ , every $τ^{'}$ , every $x \in [[τ^{'}]]$ and every $σ \in [[Γ]]$ , $[[weakenFront e τ^{'}]] (x, σ) = [[e]] σ .$

Referenced from 8 locations

A Certified Type-Preserving Compiler to Assembly

Proof of Lemma 134.8 — Weakening is denotation-preserving

Proof. Induction on $e$ , with the strengthened statement that for every insertion position $i$ the corresponding weakening satisfies the same equation. The variable case is the point: $weakenFront$ sends $First$ to $Next First$ and $Next v$ to $Next (Next v)$ , and the tuple $(x, σ)$ projects at $Next v$ exactly as $σ$ projects at $v$ . The binding cases insert at position $i + 1$ in the extended context and appeal to the strengthened hypothesis; the remaining cases are componentwise. ◻

Remark 134.9 — Why this is generated, not written ¶

Each of the six languages below needs its own $weakenFront$ , its own strengthening and substitution functions, and its own copy of lemma 134.8. None of them depends on anything specific to the language beyond its list of constructors and their binding structure. In the frozen development they are produced by a generic programming layer, together with the proofs that they commute with an arbitrary compositional denotation function. That layer, and not the compiler, is the bulk of the development.

Referenced from 3 locations

A Certified Type-Preserving Compiler to Assembly

Exercise 134.1 ¶

★☆☆ Write $weakenFront$ for the variable family $var$ , and check the two cases of lemma 134.8 for it. Say what goes wrong if $weakenFront$ is defined to send $First$ to $First$ .

Referenced from 2 locations

A Certified Type-Preserving Compiler to Assembly

Divergence and the trace domain

Definition 134.10 — The lower languages ¶

Three further languages complete the pipeline. For CPS, $\begin{aligned} τ & ::= Nat ∣ \vec{τ} \to N, & o & ::= n ∣ x ∣ λ \vec{x} : \vec{τ} . e, & e & ::= let x = o in e ∣ x \vec{y} . \end{aligned}$ For CC, $\begin{aligned} τ & ::= \dots ∣ \prod \vec{τ} ∣ \vec{τ} \times \vec{τ} \to N, & o & ::= \dots ∣ ⟨ x, \vec{y} ⟩ ∣ π_{i} x, \\ e & ::= let x = o in e ∣ x \vec{y}, & p & ::= let x = (λ \vec{y} : \vec{τ} . e) in p ∣ e . \end{aligned}$ For Alloc, $\begin{aligned} τ & ::= N ∣ ref ∣ \vec{τ} \to N, & o & ::= n ∣ x ∣ ⟨ n ⟩ ∣ new ⟨ \vec{x} ⟩ ∣ π_{i} x, \\ e & ::= let x = o in e ∣ x \vec{y}, & p & ::= let (λ \vec{y} : \vec{τ} . e) in p ∣ e . \end{aligned}$ CC hoists every function to the top level and replaces anonymous functions by closures $⟨ x, \vec{y} ⟩$ of a code pointer and an environment. Alloc makes allocation explicit, numbers the code blocks, and — the first real loss — replaces every record type by the single type $ref$ .

Referenced from 3 locations

A Certified Type-Preserving Compiler to Assembly

Scoping keeps CC terminating: a code block may call only blocks defined before it. Alloc has code pointer constants $⟨ n ⟩$ , so a block may call itself, and Alloc programs may diverge. A denotational semantics must therefore change domain exactly here.

Definition 134.11 — Traces ¶

Let $T$ be the largest set generated by $T ::= n ∣ ⊥ ∣ ⋆, T$ , that is, the coinductive type of possibly infinite sequences of $⋆$ ending, if at all, in a natural number or in $⊥$ . Write $T ↓ n$ when $T$ is a finite sequence of $⋆$ followed by $n$ . A nonterminating program denotes an infinite sequence of $⋆$ ; a program that crashes denotes a finite sequence ending in $⊥$ .

Referenced from 2 locations

A Certified Type-Preserving Compiler to Assembly

Using a coinductive stream rather than a domain-theoretic least fixed point is a decision about what can be constructed in the metatheory, not about what divergence means. It buys a definition that a total type theory accepts, at the cost that the number of $⋆$ s is observable: two programs that return the same answer after different numbers of calls have different denotations.

Definition 134.12 — Heaps, tags and failure ¶

Let $C = {Traced, Untraced} \times N$ and $M = list (list C)$ : a heap is a list of records, each field a tag together with a machine word. The tag of a type is $tagof (N) = Untraced$ , $tagof (ref) = Traced$ , $tagof (\vec{τ} \to N) = Untraced$ . Operands denote heap transformers that may fail: $\begin{aligned} [[n]] σ m & = (m, n), & [[x]] σ m & = (m, σ (x)), \\ [[⟨ n ⟩]] σ m & = (m, n + 1), & [[new ⟨ \vec{x} ⟩]] σ m & = (m \oplus [σ (\vec{x})], | m |), \end{aligned}$ and projection may fail: $[[π_{i} x]] σ m = {\begin{cases} (m, v) & if m_{σ (x), i} = (tagof (τ), v), \\ ⊥ & otherwise. \end{cases}$

Referenced from 2 locations

A Certified Type-Preserving Compiler to Assembly

The $⊥$ in the projection clause is the compensation for the type information Alloc discarded. A well-typed Alloc program never reaches it — that is part of what the preservation theorem for the CC-to-Alloc pass says — but the semantics is defined for every Alloc program, including the ones the translation cannot produce.

Exercise 134.2 ¶

★★☆ Write an Alloc program that allocates a two-field record holding a number and a code pointer, and then projects the first field expecting a $ref$ . Compute its denotation and identify the clause that yields $⊥$ . Then say why no CC program translates to it.

Referenced from 2 locations

A Certified Type-Preserving Compiler to Assembly

Closure conversion by a logical relation

Definition 134.13 — The CPS–CC relation ¶

Write $P$ and $C$ for the CPS and CC denotations. Define, by recursion on the CPS type, $\begin{aligned} n_{1} \approx_{N} n_{2} & iff n_{1} = n_{2}, \\ f_{1} \approx_{\vec{τ} \to N} f_{2} & iff \forall {\vec{x}}_{1} \in [[\vec{τ} {]]}^{P}, \forall {\vec{x}}_{2} \in [[\vec{τ} {]]}^{C} . {\vec{x}}_{1} \approx_{\vec{τ}} {\vec{x}}_{2} ⟹ f_{1} {\vec{x}}_{1} = f_{2} {\vec{x}}_{2} . \end{aligned}$

Referenced from 6 locations

A Certified Type-Preserving Compiler to Assembly

This is the ordinary logical relation for the simply typed lambda calculus, with no clause for closures at all. The reason is worth stating exactly, because it is the chapter’s one genuinely surprising step.

Remark 134.14 — Where the closure went ¶

A CC code pointer has type ${\vec{τ}}_{1} \times {\vec{τ}}_{2} \to N$ , whose denotation is $T_{1} \to T_{2} \to N$ with $T_{1}$ the denotation of the environment type. The translation of a CPS abstraction emits a fresh code block and immediately applies its denotation to the environment built from the abstraction’s free variables. That partial application has denotation $T_{2} \to N$ , which is exactly the shape definition 134.13 expects at ${\vec{τ}}_{2} \to N$ . The packaging of code with environment has been performed by a metalanguage function that already captures its free variables, so the relation never mentions it. Under an operational semantics the same proof needs existential types and a relation on packages.

Referenced from 3 locations

A Certified Type-Preserving Compiler to Assembly

Theorem 134.15 — Closure conversion is sound ¶

For every CPS term $e$ in context $Γ$ and every pair of substitutions related pointwise by definition 134.13, $[[e {]]}^{P} σ_{1}$ and $[[[[e {]]}_{C} {]]}^{C} σ_{2}$ are related at the type of $e$ .

Referenced from 4 locations

A Certified Type-Preserving Compiler to Assembly

Proof of Theorem 134.15 — Closure conversion is sound

Proof. Induction on $e$ , unfolding definition 134.13 at each type. The abstraction case is remark 134.14: the induction hypothesis relates the body under a substitution extended by related arguments, and the partial application of the emitted code block to the environment is definitionally the metalanguage function the hypothesis produced. The application case instantiates the relation at the argument, which the hypothesis for the argument supplies. The variable, constant and $let$ cases project or extend the substitution and reapply the hypothesis. ◻

A moving heap

The last translation targets an assembly language whose $new$ instruction is provided by a runtime system. That system may relocate every object in the heap on every allocation, provided it relocates the roots consistently. The proof of the last pass therefore needs a theorem saying that a well-typed program cannot observe the relocation.

Definition 134.16 — Pointer isomorphism ¶

Fix heaps $m_{1}, m_{2} \in M$ . Two words $w_{1}, w_{2}$ are isomorphic when the records $m_{1, w_{1}}$ and $m_{2, w_{2}}$ have the same length, agree field by field on tags, agree on the data of every $Untraced$ field, and have isomorphic data in every $Traced$ field.

Referenced from 2 locations

A Certified Type-Preserving Compiler to Assembly

Theorem 134.17 — Heap rearrangement safety ¶

Let $Δ$ be a register typing, $m_{1}, m_{2}$ heaps and $R_{1}, R_{2}$ register files such that

for every register $r$ with $Δ (r) = ref$ , $R_{1} (r)$ is isomorphic to $R_{2} (r)$ with respect to $m_{1}$ and $m_{2}$ ; and
for every register $r$ with $Δ (r) \neq ref$ , $R_{1} (r) = R_{2} (r)$ .

If $p$ is a Flat program with $Δ ⊢ p$ , then $[[p]] R_{1} m_{1} = [[p]] R_{2} m_{2}$ .

Referenced from 7 locations

A Certified Type-Preserving Compiler to Assembly

Read the conclusion carefully: the two sides are traces, so the theorem says that the program returns the same result, if any, and makes the same number of function calls, from any two isomorphic starting states. It is what makes the runtime system’s freedom to move objects invisible, and it is the hypothesis under which the Flat-to-assembly pass is proved. Its proof is a coinduction on the trace, with an inner induction on the instruction sequence maintaining the isomorphism through every load, store and allocation; the register typing $Δ$ is what tells the argument which registers are roots.

Exercise 134.3 ¶

★★☆ Drop hypothesis 2 of theorem 134.17 and give two states and a Flat program that distinguishes them. Then explain why the corresponding counterexample cannot be built when hypothesis 2 holds but the two heaps are merely permutations of one another.

Referenced from 2 locations

A Certified Type-Preserving Compiler to Assembly

The composed theorem, and its exact shape

Theorem 134.18 — Compiler correctness ¶

Let $m$ be a heap initialized with a closure for the top-level continuation, let $p$ point to that closure, and let $R$ map the first register to $p$ . For every Source term $e$ with $\cdot ⊢ e : Nat$ , $[[C (e)]] R m ↓ [[e]] (),$ where $C$ is the composite of the six translations.

Referenced from 6 locations

A Certified Type-Preserving Compiler to Assembly

Proof of Theorem 134.18 — Compiler correctness

Proof. Compose the soundness theorem of each pass. Each is stated as a relation between the denotation of a term and the denotation of its translation: theorem 134.7 for linearization, its analogue for the second CPS stage, theorem 134.15 for closure conversion, the analogues for Alloc and Flat, and the last pass under the hypotheses of theorem 134.17. At the top level the relation at type $Nat$ is equality of natural numbers, which turns the chain of relations into the displayed termination statement. ◻

Remark 134.19 — Why the theorem is stated only at Nat ¶

One might hope for a correctness theorem at every source type, obtained by composing the per-pass results parametrically. That composition fails. The semantics is not fully abstract: the denotations of two passes’ target languages contain metalanguage functions that are not denotations of any term, and equality of denotations at a function type quantifies over all of them. What composes instead is a weaker relation requiring functions to agree only at arguments that are denotations of terms — the move made by pre-logical relations. Theorem 134.18 is stated at $Nat$ because that is the type at which the weaker relation collapses to equality.

Referenced from 3 locations

A Certified Type-Preserving Compiler to Assembly

Definition 134.20 — The trusted computing base ¶

What must be trusted to believe theorem 134.18 for a particular output program, beyond the proof assistant, its kernel, and the toolchain and hardware that run them, is the code reached by a backward slice from the statement of that program’s correctness theorem: in the frozen development, about two hundred lines. To believe the compiler rather than one of its outputs, add the formalization of the source language, about a hundred lines more. Outside that slice lie the extraction to a functional language, the runtime system providing $new$ , and the assembler; none is verified, and theorem 134.17 is precisely the interface through which the runtime system’s behaviour is constrained.

Referenced from 2 locations

A Certified Type-Preserving Compiler to Assembly

Limits and seminar

The frozen source is Chlipala (2007) and its accompanying Coq development. The six languages of definition 134.1, definition 134.4, definition 134.10, the splicing operator, the trace domain, the tagged heap, the CPS–CC logical relation, theorem 134.17 and theorem 134.18 are its definitions and theorems, retained at their exact hypotheses. Proposition 134.2 and lemma 134.8 are local; the proofs written out here are local reconstructions, and the development’s own proofs are machine-checked scripts that discharge most cases by type-directed search rather than by the case analyses displayed above.

Five boundaries. The source language is the simply typed lambda calculus with natural numbers; there is no polymorphism, no recursion, no data other than functions and numbers, and therefore no source-level nontermination. The assembly language is idealized: unbounded registers, an abstract heap of records, and no instruction encoding. The theorem is an equality of traces, so it counts function calls; a pass that changed the number of calls would not satisfy it even if it preserved results. The theorem is stated at type $Nat$ only, for the reason in remark 134.19. And the runtime system is a parameter constrained only by the isomorphism condition of theorem 134.17; no garbage collector is verified here, and nothing above says that any particular collector satisfies that condition.

Against chapter 133, the contrast is exact. That chapter proved type preservation for five passes and, by its own proposition, nothing about behaviour. This chapter proves semantics preservation for six passes and gets type preservation for free, by proposition 134.2 — at the cost of a source language with far less in it, and of the generic infrastructure of remark 134.9.

[4]

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 134.4, then complete exercise 134.7.

Exercise 134.4 ¶

★★☆ Linearize $(λ x : Nat . x) 3$ using definition 134.5, writing every splice in full. Then verify theorem 134.7 on the result by computing both sides at the identity continuation, naming the clause used at each step.

Referenced from 3 locations

A Certified Type-Preserving Compiler to Assembly

Exercise 134.5 ¶

★★☆ Give an Alloc program whose denotation is an infinite sequence of $⋆$ , and one whose denotation is a finite sequence ending in $⊥$ . Then give two Alloc programs that return the same answer but have different denotations, and say which hypothesis of theorem 134.18 would fail if one were compiled to the other.

Referenced from 2 locations

A Certified Type-Preserving Compiler to Assembly

Exercise 134.6 ¶

★★★ Redo definition 134.13 for an operational semantics: define a step relation for CPS and for CC, and state the logical relation that theorem 134.15 would need. Identify the clause that must mention existential packages, and explain in two sentences which feature of the denotational setting removed it.

Referenced from 2 locations

A Certified Type-Preserving Compiler to Assembly

Exercise 134.7 — Practical: intrinsic syntax and splicing ¶

★★★ Practical project.ctpc-intrinsic-splice Complete project ctpc-intrinsic-splice. Implement, for the source and Linear languages of definition 134.1, definition 134.4, (i) a type checker for the source language together with a builder interface whose application constructor is defined only when its two arguments already agree at the domain type, so that an ill-typed application cannot be built through the interface, (ii) an evaluator for the source language and one for Linear terms in which a throw returns the thrown value and a call runs the callee and throws its result to the continuation, (iii) $weakenFront$ as an index shift and the splicing of definition 134.5, and (iv) a checker for the equations of lemma 134.8 and lemma 134.6 on named inputs. The invariant the implementation must maintain is that linearization is total on terms the builder accepts. If the implementation language has indexed inductive families, build the syntax intrinsically instead and delete the builder interface; if it does not, record that the type-preservation reading of proposition 134.2 is not modelled. The named cases print

identity-app: 3
linearized: 3
weaken-preserves: ok
splice-sound: ok
ill-typed-app: unrepresentable

The checker is independent evidence on the named inputs. It does not prove lemma 134.6 or lemma 134.8, implements none of the four lower languages, and contains no trace domain, heap or runtime system. One of its splice cases must have a second term that mentions a variable of the outer context; without such a case the renumbering step of definition 134.5 is not exercised at all.

Referenced from 3 locations