Wolfgang Schreiner: Thinking Programs
Logical Modeling and Reasoning about Languages, Data, Computations, and Executions
(c) 2021 Springer Texts & Monographs in Symbolic Computation
===================================================================================

ERRATA:

Due to an error in the publishing process, references across chapters are
displayed as symbolic labels (within chapters, they are correctly
displayed). In the following, we give the actual meaning of these labels:

def:logicsyntax: Definition 2.1 (page 25).
def:semanticsfo: Definition 2.16 (page 47).
def:relupdate: Definition 4.13 (page 118).
sect:structural: Section 1.2
sect:primitive: Section 5.2
sect:inductrel: Section 5.5
sect:inductrel2: Section 5.6
sect:inductfun: Section 5.7
sect:indproof: Section 5.8
chapter:models: Chapter 4
chapter:recursion: Chapter 5

Other errors:

page xxxi: in the sentence "The whole Coq specification ..." several percentage
signs are missing. It should read "The whole Coq specification consists of 42000
lines of which approximately 14 % represent the compilation algorithms, 10 %
defined the formal semantics of the various languages, and 76 % represent the
correctness proofs themselves."

page 6: the phrase "the grammar on Sect. 1.1" should be "the grammar on page 3"

page 10: the phrase "1 + mult[[E_a]] * mult[[E_b]]" at the bottom of the page
should be "1 + mult[[E_a]] + mult[[E_b]]".

page 22: the command 

  Printf.printf "

should be

  Printf.printf "%s\n" (str e2) ;;

page 208: the phrase "on Sect. 6.1" should be "in Sect. 6.1".

page 232: the phrases "head(0,[])" and "tail(0,[])" should be
"head([0,[]])" and "tail([0,[]])", respectively.

page 233: the phrase "singleton {errorL}" should be "equivalence class
[errorL]".

page 241: in Example 6.18, the last half-sentence "and that that it does not
contain different observationally equivalent streams" should be dropped.

page 241: the reference "Fig. 6.8" should be "Fig. 6.9".

page 247: in Fig. 6.10 the last two head values T and F should be exchanged
to F and T (in order to conform to the remark at the end of Example 6.22).

pages 255 and 258: the equation "Σ' = ⟨Σ.s ∪ Σ_1.s, ⟨c(...), ...⟩⟩" should be
"Σ' = ⟨s(Σ.s ∪ Σ_1.s), c(...), ...⟩".

pages 255 and 272: the phrase "for the extension morphisms ... and and ..." 
should be "for the extension morphisms ... and ..."

page 269: the phrase "spec LIST[NAT fit Elem→Nat,op→+,isE→is0]" should be
"spec LIST[NAT fit Elem→Nat,e→0,op→+,isE→is0]".

page 309: the specification line "spec MyIntCore = Nat then" should be
"spec MyIntCore = Nat then %mono".

page 310: the specification line "spec MyInt = MyIntCore then" should be
"spec MyInt = MyIntCore then %def".

page 341: at the end of the proof, the phrase "We are thus done with t(i) := s
and n := 0" should be "We are thus done with t(0) := s and n := 0".

page 342: the phrase "Then the value of the expression E := 2*x+3*y ..." should
be "Then the value of the expression E := 2*x+3*(y+1) ..."

page 347: in line 8, the phrase "From the inference rules for ->>, we thus have"
(big-step relation ->>) should be "From the inference rules for ->, we thus have"
(small-step relation ->).

In line 9, the phrase "〈E1+E2,s〉 →∗ 〈N1+E1,s〉" should be "〈E1+E2,s〉 →∗ 〈N1+E2,s〉".

page 363: the phrase "→Ms 〈13,[...c→2],...〉" should be "→Ms 〈13,[...c→3],...〉".

page 371: in Example 7.5, the last two configurations "<1, [a↦2,...], ...>"
should be "<1, [a↦3,...], ...>" and "<1, [a↦4,...], ...>", respectively.

page 372: in Example 7.6, the store "[a↦0,c↦0,c↦0]" should be "[a↦0,b↦0,c↦0]".

page 373: in the second part of Proposition 7.22, the phrase "T_a〚X〛"
should be "T_b〚X〛".

page 395: in the sentence "this tag indicates a reference parameter; where"
the word "where" should be replaced by "here".

page 396: the sentence 

  The program P itself is annotated as P^{d,p,c} where ... p is the number of
  parameters of the program, and c is the number of local variables (including
  the parameters) declared in the program.

should be

  The program P itself is annotated as P^{d,p,c} where ... p is the total number
  of global variables and parameters of the program, and c is the total number of
  global variables, parameters, and local variables declared in the program.
  
In Figure 7.21 and in the example program the annotation "main^{1,4,4}" should
be "main^{1,5,5}".

page 398: in "Rules for Sigma |- P: program", the premise "Sigma |- X:
vparams(Vt',Ss,Ap)" should be "Sigma,Ad |- X: vparams(Vt',Ss,Ap)".

The "Rules for Sigma |- X:vparams(Vt,Ss,A)" should be
"Rules for Sigma,A |- X:vparams(Vt,SS,A')" with rules

Vt = ∅  Ss = []  A' = A
-------------------------------
Sigma,A |- _: vparams(Vt,Ss,A')

Sigma,A |- X:vparams(Vt',Ss',A'') .... 
Vt = Vt' <- {<V,<S,local:A''>>} ...
A' = A''+1
-----------------------------------
Sigma,A |- X,V:S: vparams(Vt,SS,A')

In the "Rules for Sigma |- X:rparams(Vt,Ss,A)", the phrase "reference(A'')"
should be "reference:A''".

page 407: the phrase "page ??" should be "page 19".

page 408: the command

  Printf.printf "

should be

  Printf.printf "%s\n" (cstr c) ;;

page 410: the code block

  let s = update (init 0) "n" 5 ;;
  Printf.printf "
  let s0 = cval c s ;;
  Printf.printf "

should be

  let s = update (init 0) "n" 5 ;;
  Printf.printf "%s\n" (sstr s) ;;
  let s0 = cval c s ;;
  Printf.printf "%s\n" (sstr s0) ;;

page 415: the phrase "file program.imp" should be "file prog.imp".

page 546: at the end of the page, the action sequence trail 
"-> Client[0].enter() -> ..." should be
"-> Server.request(0) -> Client[0].enter() -> ...".