From System F to Typed Assembly Language

• p. 2 Section 1, paragraph 4

  including run-time code generation, intensional polymorphism, and array bounds check elimination. In Section 8 we discuss how to extend the type system presented here to support such techniques.

• p. 31 Section 8.2 Future Work

  have shown how to eliminate array bounds checks ef-

Only the authors can say what is right here.

Judge's note: Read the text of Sections 8.1 and 8.2 (pp.29–31). Bounds-check elimination is covered (Xi and Pfenning) and so is run-time type analysis (Crary et al.). Run-time code generation is not mentioned anywhere in Section 8, so the forward pointer promises more than the section delivers.

Second check: another model agreed

• p. 23 Fig. 16, rule (0-1)

  (0-1)

• p. 32 Appendix, Lemma (Subtyping Regularity)

  If ∆⊢TAL τ ≤τ ′ then ∆⊢TAL τ and ∆⊢TAL τ ′.

• p. 37 Subject Reduction, Case st, step (1)

  it follows from Subtyping Regularity and the definition of σ0 that ∅⊢TAL τj for each 0 ≤j < n

Only the authors can say what is right here.

Judge's note: My reworking from the p.23 image: take ∆=∅, n=2, i=1, τ1=int, τ2=α. The premise ∅ ⊢ int holds, since FTV(int)=∅. Rule (0-1) then gives ∅ ⊢ ⟨int^1, α^1⟩ ≤ ⟨int^0, α^1⟩. But rule (type) requires FTV ⊆ ∅, so ∅ ⊬ ⟨int^1, α^1⟩, which contradicts Subtyping Regularity on p.32 (proved only "by induction on derivations"). The st case on p.37 relies on Regularity for ∅ ⊢ τj for every j. Rules (htype) and (rftype) use an unannotated τi premise to mean "for all i". If that convention applies here too, the rule and the lemma hold, but then i is overloaded with the flipped position, so the printed rule is ambiguous rather than certainly wrong. The authors should state which reading is intended (presumably ∆ ⊢ τj for all j).

Second check: another model agreed

• p. 1 First-page footnote

  Authors’s addresses

Judge's note: Seen in the crop of the p.1 footnote. A misspelled possessive, so cosmetic only.

Second check: none (judge only)

• p. 1 Funding footnote

  ARPA/RADC grant F30602-1-0317

Only the authors can say what is right here.

Judge's note: Rests on outside knowledge: that the ARPA/RADC grant is F30602-96-1-0317. The p.1 image does show "F30602-1-0317", which has one field fewer than the AFOSR number printed next to it (F49620-97-1-0013). Only the authors can give the correct number.

Second check: none (judge only)

• p. 6 Section 3, paragraph after the λF syntax

  operated on by by

• p. 6

  operated on by by arithmetic primitives p

• p. 6

  ger literals (i), operated on by by arithmetic primitiv

Judge's note: The page image shows both words on the same line of running text, so this is not an extraction artefact.

Second check: code check

• p. 26 Corollary (Compiler Type Correctness)

  If ⊢F e : τ then

• p. 9 Lemma (CPS Conversion Type Correctness)

  If ∅; ∅⊢F e : τ

Judge's note: The crop of p.26 shows the context-free form. The text defines only ∆; Γ ⊢F e : τ (line ~331), and the CPS lemma on p.9 uses ∅;∅. This is evidently shorthand for closed terms, but it is never defined.

Second check: none (judge only)

• p. 11 Fig. 5, replaced typing rule for fix (conclusion)

  fix x[⃗α](xn:τ1, . . . , xn:τn).e

• p. 11 Fig. 5, replaced typing rule for fix (conclusion)

  ∆; Γ ⊢C fix x[⃗α](xn:τ1, . . . , xn:τn).e

• p. 11 Fig. 5, replaced typing rule for fix, conclusion

  fix x[α](xn:τ1, . . . , xn:τn).e

Judge's note: The crop shows the subscript n on the first binder of the conclusion. The premise and the introducing sentence both have x1:τ1,…,xn:τn. This is a notational slip with an evident fix.

Second check: none (judge only)

• p. 31 Section 8.2, paragraph 2

  following the work of Crary et al. [1998; 1999]

• p. 11 Section 5

  recent work of Crary et al. [1998; 1999]

• p. 40 References

  Crary, K. and Weirich, S. 1999. Flexible type analysis.

Judge's note: I read the reference list: the 1998 entry has three authors (Crary, Weirich, Morrisett) and the 1999 entry has two. Under author–year style the 1999 work should be cited as "Crary and Weirich [1999]". The intended target is unambiguous, so this is cosmetic.

Second check: none (judge only)

• p. 12 Section 5.2

  hoisting, and few simplifying optimizations

Judge's note: Seen in the crop. Two optimizations are listed (beta reduction and copy propagation), so the intended sense is "a few". Cosmetic.

Second check: none (judge only)

• p. 16 Fig. 10, heap value rule for tuples

  ∅; Γ ⊢vi : τi

Judge's note: The crop shows a bare ⊢ in the premise, while the conclusion and the surrounding rules all use ⊢A. The intended judgment is clear from context.

Second check: none (judge only)

• p. 22 Fig. 15, row for ∆⊢TAL Γ1 ≤ Γ2

  Γ1 is register file subtype of Γ2

Judge's note: Seen in the crop of the Fig. 15 table. The article is missing.

Second check: none (judge only)

• p. 23 Fig. 16, rule (reg)

  {r1 ↦ τ1, . . . , rn ↦ τn}

• p. 23 Fig. 16, rule (reg), conclusion

  {r1 7→τ1, . . . , rn 7→τn}

• p. 33 Lemma (Register File Update), proof

  Γ is {r1 7→τ1, . . ., rm 7→τm}

Judge's note: The images of pp.23 and 33 show ↦ in the register-file types. The text layer of Fig. 13 gives the colon form, and the lemma statement on p.33 uses Γ{r : τ}. This mixes notation between values and types; the meaning is still clear.

Second check: none (judge only)

• p. 29 Section 8.1, second paragraph

  are extending it to produced typed object files

• p. 29

  extending it to produced typed object files

Judge's note: The p.29 crop shows "produced" printed, so this is not an extraction artefact.

Second check: none (judge only)

• p. 32 Lemma (Heap Update), hypothesis

  Ψ{ℓ : τ} ⊢TAL h : τ then

• p. 32 Appendix, Lemma (Heap Update), hypotheses

  and Ψ{ℓ : τ} ⊢TAL h : τ then

• p. 37 Subject Reduction, Case st, step (1)

  By Heap Update it follows that Ψ′; ∅⊢TAL wj : τ

Judge's note: The p.32 image confirms that "hval" is missing in Heap Update but present in Heap Extension. A second reviewer noted that the st case (p.37) applies Heap Update to obtain Ψ′ typings before the lemma's h-hypothesis has been established. The proof of parts 3–8 uses only ∅ ⊢ τ ≤ Ψ(ℓ), so those steps are true; at most their justification is loose. That point is therefore not confirmed as a defect (it would fall under out_of_scope).

Second check: none (judge only)

• p. 32 Lemma (Heap Update), hypotheses

  Ψ{ℓ : τ} ⊢TAL h : τ then

Judge's note: On p.32 the Heap Extension hypothesis reads 'Ψ{ℓ:τ} ⊢TAL h : τ hval', while Heap Update reads 'Ψ{ℓ : τ} ⊢TAL h : τ then' without 'hval'. The heap-value judgment in Fig. 17 (p.24) is 'Ψ ⊢TAL h : τ hval'. This is a notational omission and the meaning is clear.

Second check: none (judge only)

• p. 33 Register File Update, proof

  Γ is {r1 ↦ τ1, . . ., rm ↦ τm}

• p. 33 Register File Update, statement

  Γ{r : τ}

Judge's note: On p.33 the statement uses Γ{r : τ} and the proof uses ↦. The Fig. 13 grammar is Γ ::= {r1:τ1,...}. However, the (reg) rule in Fig. 16 (p.23) also writes the register file type as {r1 ↦ τ1, ..., rn ↦ τn}, so the proof follows the paper's own rule. The notation is inconsistent across the paper, but this is cosmetic.

Second check: none (judge only)

• p. 33 Lemma (Canonical Word Forms), item (4)

  If τ = ∃α.τ then w = pack [τ′, w′] as ∃α.τ

• p. 34 Lemma (Canonical Forms), item (4)

  If τ = ∃α.τ then

• p. 34 Lemma (Canonical Forms), item (4)

  If τ = ∃α.τ then ˆR(v) = pack [τ ′, w] as ∃α.τ

Judge's note: Both items are visible on the images of p.33 and p.34. The equation τ = ∃α.τ is circular as printed. The body needs a separate name, for example ∃α.τ″, as in the unpack case of Subject Reduction, which uses ∃α.τ′. The intended meaning is recoverable.

Second check: none (judge only)

• p. 34 Lemma (Canonical Forms)

  If ⊢TAL H : Ψ hval

Judge's note: The p.34 image shows 'If ⊢TAL H : Ψ hval'. In Fig. 16 the (heap) rule concludes ⊢TAL H : Ψ, and Canonical Word Forms on p.33 states this premise correctly.

Second check: none (judge only)

• p. 35 Lemma (Register File Weakening)

  Ψ; ∆ ⊢TAL R : Γ1 then Ψ; ∆ ⊢TAL R : Γ2

• p. 34 Lemma (Canonical Forms), hypothesis

  If ⊢TAL H : Ψ hval

Judge's note: p.35 shows 'Ψ; Δ ⊢TAL R : Γ1 then Ψ; Δ ⊢TAL R : Γ2'. Fig. 16 (p.23) defines Ψ ⊢TAL R : Γ, and p.22 says 'Neither heaps nor register files may contain free type variables, so their judgments do not include a type context'. The jmp case applies the lemma to Ψ ⊢TAL R : Γ. Note 2 also raises the 'hval' on the heap judgment in Canonical Forms, which is judged under C019, and the Progress derivations, which are judged under C025.

Second check: none (judge only)

• p. 36 Subject Reduction, Case ld, item (2)

  By Register File we conclude

• p. 36 Subject Reduction, case ld, item (2)

  By Register File we conclude Ψ ⊢TAL R′ : Γ′.

Judge's note: The p.36 image shows 'By Register File' followed by a line break and then 'we conclude'. The other cases cite 'Register File Update' by its full name.

Second check: none (judge only)

• p. 36 Subject Reduction, Case ld

  H(ℓ) = ⟨w0, . . ., wm−1}

• p. 36

  H(ℓ) = ⟨w0, . . ., wm−1}, and 0 ≤i < m

Judge's note: The p.36 image shows the closing brace. Every other tuple in the paper closes with ⟩.

Second check: none (judge only)

• p. 38 Progress proof, Case halt (and other cases)

  Ψ; ∅ ⊢TAL R : Γ

Judge's note: On pp.38–39 every Progress case (halt, add/mul/sub, bnz, jmp, ld, mov, st, unpack) shows 'Ψ; ∅ ⊢TAL R : Γ'. The (prog) rule in Fig. 16 and the Subject Reduction derivations use Ψ ⊢TAL R : Γ.

Second check: none (judge only)

• p. 38 Subject Reduction, Case unpack, item (2)

  By Register File Update if follows that

Judge's note: Visible in item (2) of the unpack case on the p.38 image.

Second check: none (judge only)

• p. 38 Progress proof, Case add, mul, sub

  R(rs) and R(v) each represent integer literals

• p. 38 Appendix, proof of Progress, Case add, mul, sub

  By Canonical Forms, R(rs) and R(v) each represent integer literals.

Judge's note: The p.38 image shows R(v) without a hat, while the next line has R̂(v). The corresponding Subject Reduction case (p.36) writes R̂(v). R is defined only on registers.

Second check: none (judge only)

• p. 38 Progress proof, Case bnz

  code[α1, . . ., αn].Γ′′.I′

Judge's note: This form appears in the bnz case on the p.38 image and in the jmp case on the p.39 image. Fig. 13 and the Canonical Forms lemmas write code[α1,...,αn]Γ′.I, with no dot. Cosmetic.

Second check: none (judge only)

• p. 40 References, Dimock et al. 1997

  reprsentation transformations

• p. 40 Dimock et al. 1997 entry

  reprsentation

• p. 41 Necula and Lee 1996 entry

  USENIX Assocation

• p. 41 Shao 1997

  Chestnull Hill

Judge's note: Checked the crop and page 40: the misspelling "reprsentation" is printed in the image, so it is not an extraction artefact. This cluster also lists "Assocation" and "Chestnull", which are judged on their own in C033 and C034.

Second check: none (judge only)

• p. 40 References, Girard 1972

  Interprétation fonctionelle

• p. 40 References, Girard 1972

  Interprétation fonctionelle et élimination des coupures

Only the authors can say what is right here.

Judge's note: Rests on outside knowledge: the standard French spelling is "fonctionnelle" (double n), as is the actual thesis title. Page 40 shows "fonctionelle" with a single n.

Second check: none (judge only)

• p. 41 References, Necula and Lee 1996

  USENIX Assocation

• p. 41

  USENIX Assocation, Berkeley

Judge's note: Checked the crop of page 41: "USENIX Assocation" is printed in the image.

Second check: none (judge only)

• p. 41 References, Shao 1997

  Chestnull Hill, MA 02467-3808

• p. 41 References, Shao 1997

  Chestnull Hill, MA

Only the authors can say what is right here.

Judge's note: Rests on outside knowledge: Boston College is in Chestnut Hill, MA 02467. The crop of page 41 shows "Chestnull Hill" in print.

Second check: none (judge only)