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 teaching 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 (draft)
  • 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 (draft)
  • 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 (draft)
• Chapter 8: Domain theory (draft)
  • P179, line 2: (d_i,e_i) should be {(d_i,e_i)}
• Chapter 9: Denotational semantics of HOFL (draft)
  • P202, line 1: induction should be inductive
• Chapter 10: Equivalence between the operational and denotational semantics of HOFL (draft)
• Chapter 11: CCS, the calculus of communicating systems (draft)
  • P226, definition of ENDCELL: input on gamma should be output on gamma
  • P234, mid page: is x does should be if x does
  • P246, line 3: fro should be for
  • P247, statement of Theorem 11.4: if should be is
  • P249, line -10: (p,q_m) should be (p',q_m)
  • P256, explanation of diamond op: satisfies and the should be satisfies the
  • P264, item 1: string should be strong
• Chapter 12: Temporal logics and the mu-calculus (draft)
  • P281, end of line 3: \nu x.\mu\phi should be \nu x.\phi
  • P281, mid page: a dot is missing before This
  • P286, Problem 12.2, item 1: in should be is
• Chapter 13: Pi-calculus (draft)
  • P289, abstract: ingenuous should be ingenious
• Chapter 14: Measure Theory and Markov Chains (draft)
  • P320, line-9: X₁ should be X_t
  • P322, end of last line: a_i,i+1 should be a_si,si+1
  • P326, line -12: \mu should be l (twice)
  • P328, mid page: \gamma_M should be \gamma_D
• Chapter 15: Discrete Time Markov Chains with Actions and Non-determinism (draft)
• Chapter 16: PEPA (draft, optional reading)