DidaWiki

Questa è una vecchia versione del documento!

---

Lecture notes: a monograph is under preparation, earlier drafts of the chapters are made available here (with errata).

See main page for updated versions of the material.

• Chapter 1: Introduction (draft)
  • P17, page top: paramters should be parameters
  • P17, line above Exercise 1.2: e₀ should be e₁
  • P19, functional code: fibiter should be fibaux
• Chapter 2: Preliminaries (draft)
  • P34, page bottom: chek should be check
  • P36, Example 2.4: x in E is repeated twice in the premises, the premise y in E is missing
• Chapter 3: Operational semantics of IMP (draft)
  • P60, mid page, rightmost part of the conclusion: y:=(y+1) should be y:=(y-1)
  • P64, page bottom: while x >= 0 do x := x-1 should be while x != 0 do x := x-1
  • P66, first case: (iftt) should be (whtt)
  • P66, second case: (ifff) should be (whff)
  • P66, second case, line 1: \sigma(x)\neq 0 should be \sigma(x)=0
  • P70, end of derivation: <[] should be []
• Chapter 4: Induction and recursion (draft)
  • P78, proof of Lemma 4.1, first implication: ⇐ should be ⇒
  • P86, line -12: m₁ should be m'₁
  • P87, line -7: tha should be that
  • P88, rule 4.10: there is a misplaced dot in the premise
  • P91, line 13: 1≤i≤n should be 1≤i≤k
  • P93, mid page: the symbol c in the pair (b,c) should be existentially quantified
• Chapter 5: Partial orders and fixed points
  • P101, towards page bottom: inerently should be inherently
  • P107, Def. 5.7, line 3: of P should be of Q
  • P110, Example 5.12, line 3: n should be x
  • P112, line -3: missing closed parenthesis after “Figure 5.4”
• Chapter 6: Denotational semantics of IMP
  • P129, two lines above Def. 6.2: function. should be function,
  • P136, line -1: C[c₀] should be C[c₀]\sigma
  • P135, line -3: b should be b₀
  • P137, mid page: “of type is” should be “of type”
  • P139, Example 6.8, definition of Gamma: B[x\neq 0] should be B[x\neq 0]\sigma
• Chapter 7: Operational semantics of HOFL
• Chapter 8: Domain theory
  • P179, line 2: (d_i,e_i) should be {(d_i,e_i)}
• Chapter 9: Denotational semantics of HOFL
  • P202, line 1: induction should be inductive
• Chapter 10: Equivalence between the operational and denotational semantics of HOFL