A Theory of Type Qualifiers
Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, 1999 · paper · Computer science
Describes a framework for adding user-specified type qualifiers to a language, with qualifier inference and qualifier polymorphism. As an application, a const-inference system for C shows that real C programs could use many more consts than they do.
Checked: PDF from cs.tufts.edu, fetched 4 Oct 2026. Page numbers are those of that PDF.
3 findings
Substance Figure 4b (If) rule premises read "A ⊢ e1 : Q int A ⊢ e2 : ρ A ⊢ e2 : ρ"; the else-branch e3 in the conclusion is never typed (third premise should be A ⊢ e3 : ρ).
- p. 5 Figure 4b, rule (If)
A ⊢e1 : Q int A ⊢e2 : ρ A ⊢e2 : ρ
- p. 5 Figure 4b, (If) rule
A ⊢ e2 : ρ A ⊢ e2 : ρ
Judge's note: The page image of Figure 4b on p.5 shows e2 in both of the last two premises, while the conclusion is 'if e1 then e2 else e3 fi : ρ'. As printed, the rule does not constrain e3. The intended fix (A ⊢ e3 : ρ) is evident.
Second check: another model agreed
Report a problem with this finding
Substance (Let_v) conclusion reads "A ⊢ let x = v in e2 ni : ρ; (∃κ.C1) ∪ C2" while the body premise gives e2 : ρ2; ρ is unbound (should be ρ2).
- p. 7 Section 3.2, rule (Let_v)
A ⊢let x = v in e2 ni : ρ; (∃⃗κ.C1) ∪C2
- p. 7 rule (Letv)
A ⊢ let x = v in e2 ni : ρ; (∃κ.C1) ∪ C2
Judge's note: The page image on p.7 confirms that the premise has e2 : ρ2; C2 and the conclusion has ρ, which no premise binds. The monomorphic (Let) rule in Fig. 4b concludes with ρ2, and the proof of Theorem 1 relies on e2[x↦v] getting the same type. The evident fix is ρ2.
Second check: another model agreed
Report a problem with this finding
Reference or label [ØP97] gives "Journal of Functional Programming, 3(2):75–85, 1997", while [Mit91] gives JFP volume 1 in 1991; the volume/issue/pages for the 1997 article appear wrong.
- p. 12 References, [ØP97]
3(2):75–85, 1997.
- p. 12 References, [Mit91]
Journal of Functional Programming, 1(3):245– 285, July 1991.
- p. 12 References, [ØP97]
Journal of Functional Programming, 3(2):75–85, 1997.
Only the authors can say what is right here.
Judge's note: Rests on outside knowledge: JFP published one volume per year (vol. 3 = 1993), and Ørbæk–Palsberg 'Trust in the λ-calculus' appeared in JFP 7(6):557–591, 1997. The page image confirms the printed '3(2):75–85, 1997' and [Mit91] '1(3) ... July 1991'.
Second check: another model agreed
Report a problem with this finding
7 minor (typos and the like; most checked by the judge only)
Wording Unsoundness example: "Line 3 typechecks because we can promote the type of y to ¬nonzero int" — but under the stated rules literal 0 already has type ⊥ int = nonzero int (nonzero is negative), so the program also typechecks under (SubRef) and does not demonstrate the unsoundness.
- p. 5 Section 2.4, example after rule (Unsound)
Line 3 typechecks because we can promote the type of y to ¬nonzero int
- p. 3 Definition 2 / Figure 2
qualifier q defines a two-point lattice Lq = q ⊑ ⊤q
- p. 5 Figure 4b, rule (Int)
A ⊢ n : ⊥ int
Only the authors can say what is right here.
Judge's note: My own reworking. Definition 2 (p.3): for a negative qualifier, L_q = q ⊑ ⊤q, so the bottom of L_nonzero is nonzero itself. Figure 2 likewise puts 'nonzero' at the bottom of L. Rule (Int) (Fig. 4b) gives n : ⊥ int, so 0 : nonzero int, and the example says missing qualifiers are ⊥. With (SubRef), x and y have type ⊥ ref(nonzero int), y := 0 typechecks with no promotion, and the assertion (!x)|nonzero holds because nonzero ⊑ nonzero. The example therefore does not separate (Unsound) from (SubRef) under the printed rules. The claim that (Unsound) is unsound still stands; only the illustration fails, for example it would work with y := ¬nonzero 0. Only the authors can say which fix they intend.
Second check: another model agreed
Report a problem with this finding
Wording (Unsound) rule writes "⊢ τ1 ⪯ τ2 / ⊢ Q1 ref(τ1) ⪯ Q2 ref(τ2)" although the grammar has ref(ρ) and ⪯ is applied to qualified types (cf. SubFun, SubRef with ρ).
- p. 5 Rule (Unsound)
⊢Q1 ref (τ1) ⪯Q2 ref (τ2)
- p. 4 Section 2.4 grammar
τ ::= · · · | ref (ρ) | unit
Judge's note: Checked p.5. (SubFun) and (SubRef) use ρ in ref and in ⪯ premises, and the grammar on p.4 has ref(ρ). (Unsound) uses unqualified τ instead. This is a notational inconsistency in a counter-example rule, and the intended meaning is clear.
Second check: another model agreed
Report a problem with this finding
Wording "Rather than using annotations, we allow the qualifier designer to place restrictions at these choice points" — the alternative just discussed is the assertion e1|¬const := e2, not an annotation.
- p. 6 Section 2.4, before (Assign′)
Rather than using annotations, we allow the qualifier designer to place restrictions at these choice points.
- p. 5 Section 2.4
this re- quirement can be expressed with an assertion e1|¬const := e2
Only the authors can say what is right here.
Judge's note: P.5 proposes the assertion e1|¬const on every assignment. P.6 then says 'Rather than using annotations'. Section 2.2 defines annotations (l e) and assertions (e|l) as distinct constructs, so 'assertions' appears to be meant. A loose sense of 'annotations' is possible, so only the authors can settle it.
Second check: another model agreed
Report a problem with this finding
Wording Corollary 1 (Soundness): "If ∅ ⊢ e : ρ; C, then either e is a value or e diverges." Read literally, a typable terminating non-value, e.g. (⊥ λx.x)(⊥ 1), is neither.
- p. 7 Corollary 1 (Soundness)
If ∅⊢e : ρ; C, then either e is a value or e diverges.
Only the authors can say what is right here.
Judge's note: My own check: (⊥ λx.x)(⊥ 1) is typable by (Lam) and (App) and reduces by β in one step to the value ⊥ 1. It is therefore neither a value nor divergent, so the literal statement fails. Subject reduction plus 'stuck expressions do not typecheck' gives 'e evaluates to a value or diverges'. That is clearly the intended result, which stands, so this is a wording defect.
Second check: another model agreed
Report a problem with this finding
Typo Conclusion: "qualifier assertions to an standard language" should be "a standard language".
- p. 11 Section 7, Conclusion
qualifier assertions to an standard language
- p. 11 Conclusion
to an standard language
Judge's note: The page image (p.11, Section 7) shows 'an standard'.
Second check: none (judge only)
Report a problem with this finding
Typo Reference [KS93] spells the co-author "Michael I. Schwartzback" while Section 5 spells "Schwartzbach".
- p. 12 References, [KS93]
Nils Klarlund and Michael I. Schwartzback.
- p. 11 Section 5, Related Work
Klarlund and Schwartzbach’s graph types [KS93]
- p. 12 Reference [KS93]
Michael I. Schwartzback.
Judge's note: The image of p.12 shows 'Schwartzback' in [KS93]. The text on p.11 (line 1402) has 'Schwartzbach'. The paper is internally inconsistent.
Second check: none (judge only)
Report a problem with this finding
Typo [Wri95]: "In Lisp and Symbolic Computation 8, volume 4, pages 343–356, 1995" puts the volume number in the title and labels the issue as volume.
- p. 12 References, [Wri95]
In Lisp and Symbolic Computation 8, vol- ume 4, pages 343–356, 1995.
Only the authors can say what is right here.
Judge's note: Rests on outside knowledge: the article is in Lisp and Symbolic Computation 8(4). The page image confirms the printed form. This is a bibliographic formatting slip.
Second check: none (judge only)