Liquid Types
2008 · paper · Computer science
Introduces Liquid Types, which combine Hindley-Milner type inference with predicate abstraction to infer dependent types automatically. In the DSOLVE tool for OCaml, array-safety proofs on benchmarks needed manual annotation of under 1% of program text, down from 31%.
Checked: PDF from goto.ucsd.edu, fetched 4 Oct 2026. Page numbers are those of that PDF.
3 findings
Substance Table 1 TOTAL for DSOLVE Char is "93(1%)", but the row entries (tower 26, fft 25, gauss 67, all others 0) sum to 118.
- p. 10 Table 1, TOTAL row, DSOLVE Char column
93(1%)
- p. 10 Table 1, DSOLVE Char column (tower, fft, gauss, TOTAL)
3(1%) 93(1%)
Only the authors can say what is right here.
Judge's note: Page 10 image checked. Every other TOTAL cell in the DML and DSOLVE Line columns sums exactly over the 11 rows above it; qsort-o, qsort-d and bitv sit below the TOTAL line. Only the authors can say whether a row entry or the total is wrong. The 1% shown would hold either way.
Second check: another model agreed
Report a problem with this finding
Reference or label Example 4, after constraint (4.4), says "a subtype of the formal f inferred in Example 1", but foldn's type, including f:({0 ≤ ν ∧ ν < n}→α→α), is inferred in Example 3. Example 1 infers max.
- p. 4 Example 4, Step 2, text after constraint (4.4)
inferred in Example 1, with the curried argument len a substituted
- p. 4 Example 4, Step 2, after (4.4)
the formal f inferred in Example 1
- p. 4 Example 4, Step 2, text after constraint (4.4)
formal f inferred in Example 1
Judge's note: Page 3/4 text checked: Example 1 is Path Sensitivity (max). Example 3 (Higher-Order Functions) ends by inferring foldn :: ∀α.n:int→b:α→f:({0≤ν∧ν<n}→α→α)→α. Step 1 of Example 4 itself calls this 'the type computed in the previous example'. The pointer should say Example 3.
Second check: another model agreed
Report a problem with this finding
Wording The un-normalized sum example in Section 4.4, "let rec sum k = if k < 0 then 0 else (s + sum (k-1))", uses the unbound variable s; k + sum (k-1) is meant.
- p. 9 Section 4.4, item 3 (A-Normalization)
let rec sum k = if k < 0 then 0 else (s + sum (k-1))
Judge's note: Crop checked. Figure 1 defines sum with 'let s = sum (k-1) in' followed by s + k. In the one-line version nothing binds s, and the text calls it the sum example from Section 2.
Second check: another model agreed
Report a problem with this finding
8 minor (typos and the like; most checked by the judge only)
Substance Table 1 TOTAL for Size Line is "633", but the 11 rows sum to 632.
- p. 10 Table 1, TOTAL row, Size Line column
633
- p. 10 Table 1, TOTAL row, Size Line
TOTAL 633
Only the authors can say what is right here.
Judge's note: Page 10 image checked. The Char column sums exactly to 14188, and the DML totals 125 and 6387 also match. The discrepancy is one line and does not change the printed 17%/31% figures.
Second check: another model agreed
Report a problem with this finding
Wording Table 1 percentages are undefined in the caption and use different bases. The DML rows use annotation/(size+annotation) (dotprod "3 (30%)" = 3/10), while bitv "65 (15%)" and "3138 (29%)" match annotation/size.
- p. 10 Table 1, bitv row
65 (15%)
- p. 10 Table 1, dotprod row, DML Line
3 (30%)
Only the authors can say what is right here.
Judge's note: Recomputed from the page 10 image. The DML entries match annotation/(size+annotation), as does the 31% headline (6387/20575). The bitv entries only match annotation/size; on the other base they would be about 13% and 23%. The caption does not define the percentages.
Second check: another model agreed
Report a problem with this finding
Wording No single rounding rule reproduces all the DSOLVE percentages in Table 1: qsort-d "5 (5%)" (4.3–4.5%), tower "1 (2%)" (2.7–2.8%) and gauss "67 (2%)" (2.7–2.8%).
- p. 10 Table 1, qsort-d row, DSOLVE Line
5 (5%)
- p. 10 Table 1, tower row, DSOLVE Line
1 (2%)
- p. 10 Table 1, gauss row, DSOLVE Char
67 (2%)
Only the authors can say what is right here.
Judge's note: Recomputed with both candidate bases. Rounding to nearest would give 4%, 3% and 3%. Truncation would explain tower and gauss, but not qsort-d or fft 1 (1%) (0.93%). Only the authors can say how these were computed.
Second check: another model agreed
Report a problem with this finding
Typo Stray article on p.1: "the run-time value of i is an always an integer between 1 and 99" should read "is always an integer".
- p. 1 Introduction, paragraph 3
the run-time value of i is an always an integer between 1 and 99
- p. 1 Introduction, para 3
is an always an integer between 1 and 99
Judge's note: The page 1 crop shows the wording exactly as quoted, so this is not an extraction artefact.
Second check: none (judge only)
Report a problem with this finding
Typo Duplicated word on p.6: "the validity of the embedded implication implies the the standard, weaker, exact requirement".
- p. 6 Section 3.3, item 2 (Decidable, Conservative Subtyping)
implies the the standard, weaker, exact
- p. 6
embedded implication implies the the standard, weaker, e
Judge's note: The page 6 crop shows 'the the' within a single line of running text.
Second check: code check
Report a problem with this finding
Typo In the blit listing, the line ending "offset1 + c > v1.length" is followed by "offset2 < 0 || ..." with no || between them, so the guard does not parse as OCaml.
- p. 10 Case Study: Bit Vectors, blit code listing
offset1 + c > v1.length
Judge's note: The crop shows no operator at the end of the first line or the start of the continuation line.
Second check: none (judge only)
Report a problem with this finding
Typo Missing word in the Conclusions: "can significantly reduce the amount manual annotation required" should read "the amount of manual annotation".
- p. 11 Section 7, first paragraph
reduce the amount manual annotation required
- p. 11 Section 7 Conclusions, first sentence
significantly reduce the amount manual annotation
Judge's note: The page 11 crop shows the wording exactly as quoted.
Second check: none (judge only)
Report a problem with this finding
Typo Reference [19] (Lincoln and Mitchell) gives the venue location as "Albequerque, New Mexico, 1992". The city is spelled Albuquerque.
- p. 11 Reference [19]
Albequerque, New Mexico
- p. 11 References, entry [19]
Albequerque, New Mexico, 1992
Only the authors can say what is right here.
Judge's note: Rests on outside knowledge: the New Mexico city is spelled 'Albuquerque'. I looked at the crop image of the reference list on PDF page 11. Entry [19] reads "P. Lincoln and J. C. Mitchell. Algorithmic aspects of type inference with subtypes. In POPL, Albequerque, New Mexico, 1992." The misspelling appears in the printed reference itself, so it is not an extraction artefact. Both crops (a and b) show the same region and cite the same defect, so they are one cluster.
Second check: none (judge only)