In Programming Logics for Certified Compilers book, on page #23, in the expression :
(v ≠ 0 ∧ ∃σ' ∃h∃t. σ = h · σ' ∧ v.head->h ∗ v.next->t ∗ listrep σ (t, 0))
It seems to me, that, since σ represents the whole list v, and σ' represents tail, the last expression should be: listrep σ' (t, 0)
. Is that correct, and it's just a misprint in the book?
Yes, you are right; it should be sigma-prime.