Errata for "Static Determination of Quantitative Resource Usage for Higher-Order Programs" by Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond and Martin Hofmann, published at POPL 2010 (Madrid).

This version of the paper has been revised in July 2010 to correct a minor mistake (and contains an appendix explaining the change), which had been discovered later by the authors themselves. The memory consistency invariant is switched from a truncated inductive definition to its proper co-inductive definition. The statements of the theorem and all lemmas remain unchanged. However, the (omitted) proofs of two lemmas need to be changed and required co-induction accordingly.

Note that using a co-inductive definition for tracking the consistency of memory configurations is not at all new: Milner and Tofte used a co-inductive definition for their consistency invariant for the same reasons in 1991 in their work "Co-induction in relational semantics". However, we had hoped to avoid a co-inductive definition for memory consistency in our case, since all infinite derivations can only mention a finite number of statements and must thus lead to repetition. Truncating these repetitions then leads to finite derivations. However, we discovered that the truncated consistency statment did not exclude certain artifical degenerated configurations, which required one more unfolding of the repetition. Eventually, we found it easier to switch to proper co-induction.

Steffen Jost, July 2010.

---

Type Rule (Var) is missing an additional cost constant, since it is also possible here that dereferencing an indirection becomes necessary. Accordingly, the rule should be
  x:A |--KpushVar+Knext-- x:A | 0
  
Steffen Jost, July 2017.