Chapter 15Optional

MixML, Recursive Linking, and Definedness

Prerequisites. Direct starred prerequisites: Chapter 12. No later core chapter depends on this route.

A component needed before it can be defined

Consider two modules. A lexer exports tokens but imports a table of keywords; a parser exports that table but imports tokens. $\begin{array}{ccc} imports & exports \\ Lexer & keywords : Table & token : Char \to Token \\ Parser & token : Char \to Token & keywords : Table \end{array}$ An ordinary functor can break this cycle only by choosing one direction first. Recursive linking must instead connect both pairs of components and must still prevent the lexer from reading $keywords$ while its slot is empty.

Definition 15.1 — The finite linking calculus Mix_0 ¶

Let $p$ range over finite component paths and let $A$ range over the pure core types of chapter 12. A polar component is $p^{-} : A$ , an import, or $p^{+} : A$ , an export. A signature $Σ$ is a finite map from paths to polar components. Modules are generated by $\begin{aligned} M, N ::= & imp (p : A) ∣ def (p = e : A) ∣ {ℓ = M} ∣ M with N \\ ∣ {seal}_{Σ} (M) ∣ complete (M) . \end{aligned}$ Paths in a nested structure are prefixed by its label. A core expression records finite sets $rd (e)$ and $wr (e)$ of slots read and written during initialization. The fragment requires $wr (e) = {p}$ in $def (p = e : A)$ .

Referenced from 3 locations

The polarity belongs to a component occurrence, not to its core type. Thus $p^{-} : A$ and $p^{+} : A$ may be linked, while two exports at the same path are competing definitions.

Definition 15.2 — Compatible signatures ¶

For signatures $Σ_{1}, Σ_{2}$ , write $merge (Σ_{1}, Σ_{2}) = Σ$ when, at every path $p$ :

a component occurring on one side only is copied to $Σ$ ;
equal-typed components of opposite polarity become the export $p^{+} : A$ ;
two imports of the same type remain the import $p^{-} : A$ ; and
two exports, or two components with different types, make the merge undefined.

The path sets are finite, so merge is a partial algorithm.

Referenced from 4 locations

For the running family, prefixing gives $\begin{aligned} Σ_{L} & = {{keywords}^{-} : Table, {token}^{+} : Char \to Token}, \\ Σ_{P} & = {{token}^{-} : Char \to Token, {keywords}^{+} : Table} . \end{aligned}$ Both opposite-polarity pairs disappear as imports, hence $merge (Σ_{L}, Σ_{P}) = {{keywords}^{+} : Table, {token}^{+} : Char \to Token} .$

Exercise 15.1 — Merge is functional and commutative ¶

★☆☆ Prove that if $merge (Σ_{1}, Σ_{2}) = Σ$ and $merge (Σ_{1}, Σ_{2}) = Σ^{'}$ , then $Σ = Σ^{'}$ . Prove also that defined merge is commutative. Explain why left bias between two equal-typed exports cannot be observed in this signature: signature entries carry a polarity and a type, not an implementation value. Finally replace the rejection of unequal overlapping components by left bias and give a one-path counterexample to commutativity.

Referenced from 3 locations

Compatibility solves the static wiring problem but not initialization. If $token$ is evaluated before $keywords$ , its initializer may read an empty slot even though the final signature is complete.

Definedness is a state transition

Definition 15.3 — Initialization judgment ¶

Let $Ω$ be a finite map from slots to core types, and let $D$ be a finite subset of $dom (Ω)$ . Write $Ω; D ⊢_{core} e : A$ when ordinary core typing gives $e : A$ and $rd (e) \subseteq D$ . The judgment $Ω; D ⊢ M : Σ \Rightarrow D^{'}$ means that $M$ has signature $Σ$ , reads only slots in $D$ , writes each absent slot at most once, and leaves exactly the slots $D^{'}$ defined. Its primitive rules for imports, definitions, and sequencing are

Ω (p) = A

Ω; D ⊢ imp (p : A) : {p^{-} : A} \Rightarrow D

Mix-Imp

Ω (p) = A

Ω; D ⊢_{core} e : A

p \notin D

wr (e) = {p}

Ω; D ⊢ def (p = e : A) : {p^{+} : A} \Rightarrow D \cup {p}

Mix-Def

Ω; D ⊢ M : Σ_{1} \Rightarrow D_{1}

Ω; D_{1} ⊢ N : Σ_{2} \Rightarrow D_{2}

merge (Σ_{1}, Σ_{2}) = Σ

Ω; D ⊢ M with N : Σ \Rightarrow D_{2}

Mix-With

For a label $ℓ$ , let $ℓ \cdot (-)$ prefix every path in a map or set. Let $ℓ^{- 1} Ω$ and $ℓ^{- 1} D$ select the entries below $ℓ$ and remove that prefix. Thus $ℓ^{- 1} D = {q ∣ ℓ . q \in D}$ . For a finite visible path set $Q$ , let $Σ |_{Q}$ restrict a signature. The remaining rules are

ℓ^{- 1} Ω; ℓ^{- 1} D ⊢ M : Σ \Rightarrow D_{0}

Ω; D ⊢ {ℓ = M} : ℓ \cdot Σ \Rightarrow (D ∖ ℓ \cdot (ℓ^{- 1} D)) \cup ℓ \cdot D_{0}

Mix-Struct

Ω; D ⊢ M : Σ \Rightarrow D^{'}

Q \subseteq dom (Σ)

Σ |_{Q} = Σ_{0}

Ω; D ⊢ {seal}_{Σ_{0}} (M) : Σ_{0} \Rightarrow D^{'}

Mix-Seal

Ω; D ⊢ M : Σ \Rightarrow D^{'}

\forall p \in dom (Σ) . \exists A . Σ (p) = p^{+} : A

Ω; D ⊢ complete (M) : Σ \Rightarrow D^{'}

Mix-Complete

Sealing hides paths only after checking the body; it does not erase their initialized cells from $D^{'}$ .

Referenced from 3 locations

The slice formulation lets sibling structures share one ambient state without requiring that state to carry two different outer prefixes. For example, let $Ω_{L P}$ contain $Lexer . token : Char \to Token$ and $Parser . keywords : Table$ , and choose initializers with empty read sets. Put $\begin{aligned} L_{0} & = {Lexer = def (token = t_{0} : Char \to Token)}, \\ P_{0} & = {Parser = def (keywords = k_{0} : Table)} . \end{aligned}$ Their signatures are $Σ_{L}^{0} = {{Lexer . token}^{+} : Char \to Token}$ and $Σ_{P}^{0} = {{Parser . keywords}^{+} : Table}$ . Two uses of Mix-Struct, followed by Mix-With, give $\begin{aligned} Ω_{L P}; \emptyset & ⊢ L_{0} : Σ_{L}^{0} \Rightarrow {Lexer . token}, \\ Ω_{L P}; {Lexer . token} & ⊢ P_{0} : Σ_{P}^{0} \Rightarrow {Lexer . token, Parser . keywords} . \end{aligned}$ Their signatures have disjoint paths, so their sequential composition merges.

The order of Mix-With matters operationally. Define the keyword table without reading $token$ , then define the token function while reading $keywords$ : write $K = def (keywords = k : Table)$ and $T = def (token = t : Char \to Token)$ . Then

Ω; \emptyset ⊢ K : Σ_{k} \Rightarrow {keywords}

Ω; {keywords} ⊢ T : Σ_{t} \Rightarrow {keywords, token}

merge (Σ_{k}, Σ_{t}) = Σ

Ω; \emptyset ⊢ K with T : Σ \Rightarrow {keywords, token}

Mix-With

The reverse order has no derivation when $keywords \in rd (t)$ , because the subset premise of Mix-Def fails.

Lemma 15.4 — Definedness grows exactly by writes ¶

If $Ω; D ⊢ M : Σ \Rightarrow D^{'}$ , then $D \subseteq D^{'}$ , and every path in $D^{'} ∖ D$ is written exactly once by $M$ .

Referenced from 5 locations

Proof of Lemma 15.4 — Definedness grows exactly by writes

Proof. Proceed by rule induction. Mix-Imp adds no path. In Mix-Def, the side condition $p \notin D$ gives $D \subseteq D \cup {p}$ , and the singleton write set gives the exact new write. In Mix-With, the induction hypotheses give $D \subseteq D_{1} \subseteq D_{2}$ . A path in $D_{2} ∖ D$ lies either in $D_{1} ∖ D$ or in $D_{2} ∖ D_{1}$ . The two sets are disjoint, and the corresponding induction hypothesis gives its unique write. In the structure case, entries outside the $ℓ$ -slice are unchanged, while prefixing injectively transports the premise’s new writes inside the slice. The two regions are disjoint, so both claims follow. Sealing does not change execution, and completeness adds no write. ◻

Lemma 15.5 — No read before definition ¶

If $Ω; D ⊢ M : Σ \Rightarrow D^{'}$ , then every read performed while initializing $M$ names a slot defined earlier in the same sequential trace or a slot in $D$ .

Referenced from 3 locations

Proof of Lemma 15.5 — No read before definition

Proof. Rule induction fixes the temporal order. Imports perform no read. For a definition, the core judgment’s read condition is exactly the claim. For Mix-With, apply the first induction hypothesis from $D$ to $D_{1}$ , then the second from $D_{1}$ to $D_{2}$ . The remaining rules preserve the trace and merely change path prefixes or visibility. ◻

Exercise 15.2 — The missing side condition ¶

★☆☆ Delete $p \notin D$ from Mix-Def. Construct a derivable module that seals its first definition to the empty visible signature and then assigns the same slot again. Explain why the seal makes signature merge defined, and identify the exact clause of lemma 15.4 that becomes false.

Referenced from 3 locations

An ordered slot trace

The finite module judgment rejects an early read by threading the set $D$ . The following command calculus isolates that stronger, ordered-initialization property. It is a teaching calculus, not the full LTG typing judgment.

Definition 15.6 — Ordered slot commands and extracted traces ¶

Write $L, U$ for the empty-cell and filled-cell modes. A mode environment $Ξ$ is a finite map of bindings $x : A^{L}$ or $x : A^{U}$ . Values are pure: the auxiliary judgment $Ξ^{U} ⊢_{v} v : A$ may inspect only the unrestricted projection $Ξ^{U}$ of $Ξ$ . Commands and scoped event traces are $\begin{aligned} c & ::= return v ∣ get x ∣ set x v ∣ c_{1}; c_{2} ∣ {new}_{A} (x . c), \\ t & ::= ϵ ∣ get x ∣ set x ∣ t_{1} \cdot t_{2} ∣ ν x . t . \end{aligned}$ The judgment $Ξ ⊢ c : B \Rightarrow Ξ^{'} ▹ t$ both checks a command and extracts its trace:

Ξ^{U} ⊢_{v} v : A

Ξ ⊢ return v : A \Rightarrow Ξ ▹ ϵ

Slot-Return

Ξ = Ξ_{0}, x : A^{U}

Ξ ⊢ get x : A \Rightarrow Ξ ▹ get x

Slot-Get

Ξ = Ξ_{0}, x : A^{L}

Ξ_{0}^{U} ⊢_{v} v : A

Ξ ⊢ set x v : 1 \Rightarrow Ξ_{0}, x : A^{U} ▹ set x

Slot-Set

Ξ ⊢ c_{1} : 1 \Rightarrow Ξ_{1} ▹ t_{1}

Ξ_{1} ⊢ c_{2} : B \Rightarrow Ξ_{2} ▹ t_{2}

Ξ ⊢ c_{1}; c_{2} : B \Rightarrow Ξ_{2} ▹ t_{1} \cdot t_{2}

Slot-Seq

x \notin dom (Ξ) \cup dom (Ξ^{'})

Ξ, x : A^{L} ⊢ c : B \Rightarrow Ξ^{'}, x : A^{U} ▹ t

Ξ ⊢ {new}_{A} (x . c) : B \Rightarrow Ξ^{'} ▹ ν x . t

Slot-New

Thus allocation creates one local $L$ -mode obligation, setting changes that mode to $U$ , and leaving the scope requires the obligation to have been discharged.

Referenced from 6 locations

Definition 15.7 — Trace validation ¶

The judgment $Ξ ⊢_{tr} t \Rightarrow Ξ^{'}$ is generated by

Ξ ⊢_{tr} ϵ \Rightarrow Ξ

Tr-Empty

Ξ = Ξ_{0}, x : A^{U}

Ξ ⊢_{tr} get x \Rightarrow Ξ

Tr-Get

Ξ = Ξ_{0}, x : A^{L}

Ξ ⊢_{tr} set x \Rightarrow Ξ_{0}, x : A^{U}

Tr-Set

Ξ ⊢_{tr} t_{1} \Rightarrow Ξ_{1}

Ξ_{1} ⊢_{tr} t_{2} \Rightarrow Ξ_{2}

Ξ ⊢_{tr} t_{1} \cdot t_{2} \Rightarrow Ξ_{2}

Tr-Seq

x \notin dom (Ξ) \cup dom (Ξ^{'})

Ξ, x : A^{L} ⊢_{tr} t \Rightarrow Ξ^{'}, x : A^{U}

Ξ ⊢_{tr} ν x . t \Rightarrow Ξ^{'}

Tr-New

A trace is safe precisely when this partial validation judgment is derivable.

Referenced from 5 locations

Proposition 15.8 — Ordered slot-trace safety ¶

If $Ξ ⊢ c : B \Rightarrow Ξ^{'} ▹ t$ , then $Ξ ⊢_{tr} t \Rightarrow Ξ^{'}$ . Consequently each $get x$ in $t$ occurs while $x$ has mode $U$ , and between an allocation $ν x$ and the end of its scope there is exactly one $set x$ .

Referenced from 3 locations

MixML, Recursive Linking, and Definedness

Proof of Proposition 15.8 — Ordered slot-trace safety

Proof. Induct on the command derivation. Return, get, and set select the corresponding trace rule. Composition applies the two induction hypotheses in sequence. For allocation, the induction hypothesis validates the body from $x : A^{L}$ to $x : A^{U}$ , so Tr-New closes the scoped trace.

For the consequence, inspect a validation derivation. Only Tr-Get emits a get, and its premise requires mode $U$ . Only Tr-Set changes the local mode; it requires $L$ and produces $U$ , so it cannot occur twice. Rule Tr-New requires that one such change has occurred before the scope closes. ◻

The full LTG boundary includes black holes

The source target uses linearity for single assignment and eventual definition, but deliberately does not enforce the temporal read discipline of definition 15.6.

Definition 15.9 — The load-bearing LTG store interface ¶

In LTG, modes are $ι ::= L ∣ U$ . Among its types and terms are reference types $(? τ)^{ι}$ , allocation $new τ$ , definition $def e_{1} := e_{2}$ , and dereference $! e$ . The full calculus also has moded kinds, functions, records, universal and existential types, fresh type names, and type-name definition. The run-time categories relevant here are $\begin{aligned} σ & ::= ϵ ∣ σ, α : ? κ ∣ σ, α := τ : κ, \\ s & ::= ϵ ∣ s, x : ? τ ∣ s, x := e : τ, \\ ξ & ::= σ; s; e ∣ ∙ . \end{aligned}$ The value-store reductions include $\begin{aligned} σ; s; E [new τ] & ⇝_{0} σ; s, x : ? τ; E [x], \\ σ; s_{1}, x : ? τ, s_{2}; E [def x := e] & ⇝_{0} σ; s_{1}, x := e : τ, s_{2}; E [{}], \\ σ; s_{1}, x := e : τ, s_{2}; E [! x] & ⇝_{0} σ; s_{1}, x := e : τ, s_{2}; E [e], \\ σ; s_{1}, x : ? τ, s_{2}; E [! x] & ⇝_{0} ∙ . \end{aligned}$ Store typing assigns $(? τ)^{L}$ to $x : ? τ$ and $(? τ)^{U}$ to $x := e : τ$ . Definition consumes an $L$ -mode capability, while dereference requires a $U$ -mode occurrence. Crucially, LTG splitting contains $(? τ)^{L} * (? τ)^{U} = (? τ)^{L} .$ Hence an unrestricted read capability may coexist with the linear obligation to fill the cell. LTG permits an early dereference, which reduces to $∙$ ; its type safety theorem does not remove that outcome.

Referenced from 4 locations

MixML, Recursive Linking, and Definedness

The ordered trace checker can be used before LTG elaboration: map an empty slot to mode $L$ , a filled slot to mode $U$ , and accept only traces validated by definition 15.7. Equation (15.1) is intentionally absent from that checker. Thus proposition 15.8 proves a local initialization-order property, while the published LTG result proves a different single-assignment-and-progress property.

Three passes and the exact imported boundary

The full MixML rules are declarative: linking chooses locators and fresh type names. A checker must remove that nondeterminism without changing which modules are typable. The source construction separates three questions.

Definition 15.10 — Full MixML semantic-signature shell ¶

The paper leaves the core constructor grammar parametric. Let $A$ range over the selected core’s beta-normal, eta-long semantic constructors, equipped with the paper’s decidable kinding, elaboration, subtyping, and substitution judgments. Relative to that explicit parameter, the complete MixML semantic objects used by the imported rules are $\begin{aligned} Σ & ::= [[= A]] ∣ [[A {]]}^{\pm} ∣ [[Φ {]]}^{\pm} ∣ {| ℓ : Σ |}, \\ Φ & ::= \forall \bar{α} . \exists \bar{β} . (L_{i}; L_{e}; Σ), \\ L & ::= [[= α]] ∣ {| ℓ : L |}, R ::= [[= A]] ∣ {| ℓ : R |}, \\ Γ & ::= ϵ ∣ Γ, X : | Σ | . \end{aligned}$ Here $[[A {]]}^{-}$ and $[[A {]]}^{+}$ are term imports and exports; unit components have the same polarities. Type imports and abstract type exports are represented by the two locators in $Φ$ . Absolute signature $| Σ |$ changes polar imports to exports before storing a module in $Γ$ . Realizer disjoint union is written $R_{1} ⊎ R_{2}$ , and $R # Σ$ means disjoint path domains.

Template erasure retains kinds and shapes: $S ::= [[κ]] ∣ [[F {]]}^{\pm} ∣ {| ℓ : S |}, F ::= L^{T}; \bar{κ}; S .$ It erases atomic term components, replaces type definitions by their kinds, and commutes with path domains, absolute signatures, locator restriction, and disjoint union. These are the full semantic categories of the imported judgments; they are not the polar path maps of ${Mix}_{0}$ .

Referenced from 6 locations

Definition 15.11 — Three-pass interface ¶

For the full source syntax of Rossberg and Dreyer, the three passes are

$Γ^{T} ⊢ M \Rightarrow L^{T}; \bar{κ}; S$ computes component domains, locator shapes, polar unit shapes, and export kinds while erasing atomic term components;
$Γ; R; \bar{β} ⊢_{stat} M : Σ_{s}$ computes static type components with the template-fixed locator and export-kind choices; and
$Γ; R; \bar{β} ⊢_{main} M : Σ ⇝ e$ checks core terms and produces LTG evidence $e$ .

Here $⇝$ is evidence elaboration, not evaluation. All three judgments use the paper’s full semantic signatures, locator disjointness conditions, freshness conditions, and analysis/synthesis well-formedness classes.

Referenced from 2 locations

MixML, Recursive Linking, and Definedness

The deterministic link rule makes the interaction of the passes inspectable. For $(X = M_{1}) with M_{2}$ , template computation first produces $\begin{aligned} Γ^{T} & ⊢ M_{1} \Rightarrow R^{T} ⊎ R_{1}^{T} ⊎ L_{1}^{T}; {\bar{κ}}_{β_{1}}; S_{1}, \\ Γ^{T}, X : | S_{1} | & ⊢ M_{2} \Rightarrow R^{T} ⊎ R_{2}^{T} ⊎ L_{2}^{T}; {\bar{κ}}_{β_{2}}; S_{2}, \end{aligned}$ with $(R_{1} ⊎ L_{1}) # (R_{2} ⊎ L_{2})$ . These domains determine the common external imports $R$ , the unmatched imports $R_{1}, R_{2}$ , and the cross-linked locators $L_{1}, L_{2}$ ; no pass guesses that partition again. The static premise checks $Γ, X : | Σ_{1} |; R ⊎ R_{2} ⊎ L_{2}; {\bar{β}}_{2} ⊢_{stat} M_{2} : Σ_{2}^{0}$ and bidirectional lookup computes the unique normalizing substitution $(L_{1}; Σ_{1}) ⋈ (L_{2}; Σ_{2}^{0}) ⟹ δ .$ The main premises then check $M_{1}$ at $Σ_{1}$ , recheck $M_{2}$ under $δ Γ, X : | δ Σ_{1} |$ and $δ L_{2}$ at $Σ_{2}$ , and finish with the deterministic merge $δ Σ_{1} + Σ_{2} ⟹ Σ .$ Equations (15.2)–(15.5) are the mechanism of the paper’s Link-Det rule: templates fix domains and fresh-kind arities, the static pass exposes type equations, lookup computes $δ$ , and the main pass checks values with those equations available.

On the lexer–parser family, the template contains two paths with opposite polarities. The static pass checks that both occurrences of $keywords$ have type $Table$ and both occurrences of $token$ have type $Char \to Token$ . The main pass then emits two cells, wires each import to the corresponding export, and sequences the initializers in an order accepted by the LTG modes.

Theorem 15.12 — Full MixML/LTG theorem boundary; exact import ¶

For the MixML and LTG signatures of Rossberg–Dreyer, including their well-formed analysis and synthesis signatures and the assumed sound and complete algorithms for the chosen pure core language, the following results hold.

Evidence translation is complete and sound: the paper’s Theorems 8.1 and 8.7 relate declarative MixML derivations to well-typed LTG terms.
Template computation is complete (Theorem 9.8), and the three-pass algorithm is complete and sound (Theorems 9.9 and 9.10).
MixML type checking is decidable and inferred signatures are unique (Corollary 9.11 and Theorem 9.12).
LTG preservation and progress are Theorems 7.10 and 7.14. A well-typed non-error configuration either steps or is a value configuration whose term and type cells are all defined. Dereferencing an undefined cell may step to $∙$ , as displayed in definition 15.9.

Referenced from 4 locations

MixML, Recursive Linking, and Definedness

Proof of Theorem 15.12 — Full MixML/LTG theorem boundary; exact import

Proof. This theorem imports the named results from [RD13]. The bridge is literal: definition 15.10 reproduces the complete MixML semantic and template shells of Figures 4, 8, and 25 relative to their stated core parameter; (15.2)–(15.5) reproduce the premises that replace declarative linking in Link-Det of Figure 29; and definition 15.9 reproduces the reference-store fragment of Figures 13–15. Consequently a derivation of the displayed three-pass judgments is a derivation in the hypotheses of Theorems 9.8–9.10, and its evidence conclusion is the input of Theorems 8.1 and 8.7.

The theorem is not obtained from ${Mix}_{0}$ or from the ordered trace checker. The source proofs use environment-splitting substitution for LTG, analysis/synthesis well-formedness for elaboration, deterministic signature approximation for the static pass, and deterministic shapes for template completeness. These hypotheses are retained because removing any one changes the source judgment or invalidates its induction. ◻

Remark 15.13 — No transfer to Standard ML ¶

The theorem concerns the frozen MixML/LTG pair. Standard ML lacks MixML’s polar semantic signatures and is not translated by the stated evidence judgments. Dreyer’s recursive-module calculus and Leroy’s modular module system give useful predecessor comparisons, but their soundness results do not instantiate theorem 15.12.

Referenced from 2 locations

MixML, Recursive Linking, and Definedness

Exercise 15.3 — Classify the claims ¶

★★☆ For each claim, state whether theorem 15.12 establishes it and name the decisive hypothesis: (i) a successful full MixML elaboration is LTG-typed; (ii) every Standard ML recursive module is safe; (iii) a non-error terminal LTG module has no empty component; (iv) arbitrary impure core-language extensions preserve completeness. State separately what can happen after an early dereference.

Referenced from 3 locations

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 15.4, then implement exercise 15.6.

Exercise 15.4 — A rejected recursive family ¶

★★☆ Give signatures for the lexer–parser family and calculate their merge. Then use initializers with $rd (k) = {token}$ and $rd (t) = {keywords}$ . Prove that neither sequential order has an initialization derivation, although the merged signature is complete.

Referenced from 4 locations

Exercise 15.5 — Two notions of completeness ¶

★★☆ Construct a module whose merged signature has only exports but whose chosen initializer order fails. State separately signature completeness and LTG definedness, and prove that neither definition implies the other without an elaboration-soundness premise.

Referenced from 3 locations

Exercise 15.6 — Definedness checker ¶

★★★ Practical project.mixml-checker Implement in Kappa a finite ${Mix}_{0}$ merge and initialization checker. Maintain the invariant that the state set contains exactly the slots written by the accepted prefix. The program must accept the ordered keyword/token family, reject its early-read reversal, reject duplicate exports, reject a type mismatch, and reject a cyclic pair in both orders. The exact five-case output recorded in appendix E is the acceptance test; an empty Kappa audit is also required.

Referenced from 5 locations

Exercise 15.7 — A disciplined extension ¶

★★★ Define a parallel composition rule for two modules whose read/write sets are independent. State the independence condition, prove that either sequential order is derivable under that condition, and show by counterexample why disjoint write sets alone do not suffice.

Referenced from 3 locations