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

See [[magistraleinformatica:mod:start|main page]] for updated versions of the teaching material.

     * {{:magistraleinformatica:mod:01-introduction-draft-2016.pdf|Chapter 1}}: Introduction (draft)
      * P17, page top: paramters should be parameters
      * P17, line above Exercise 1.2: e<sub>0</sub> should be e<sub>1</sub>
      * P19, functional code: fibiter should be fibaux
    * {{:magistraleinformatica:mod:02-preliminaries-draft-2016.pdf|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
    * {{:magistraleinformatica:mod:03-imp-opsem-draft-2016.pdf|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 []
    * {{:magistraleinformatica:mod:04-induction-draft-2016.pdf|Chapter 4}}: Induction and recursion (draft)
      * P78, proof of Lemma 4.1, first implication: <= should be =>
      * P86, line -12: m<sub>1</sub> should be m'<sub>1</sub>
      * 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
    * {{:magistraleinformatica:mod:05-cpo-draft.pdf|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"
    * {{:magistraleinformatica:mod:06-imp-densem-draft-2016.pdf|Chapter 6}}: Denotational semantics of IMP (draft)
      * P129, two lines above Def. 6.2: function. should be function,
      * P136, line -1: C[c<sub>0</sub>] should be C[c<sub>0</sub>]\sigma
      * P135, line -3: b should be b<sub>0</sub>
      * 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
    * {{:magistraleinformatica:mod:07-hofl-opsem-draft-2016.pdf|Chapter 7}}: Operational semantics of HOFL (draft)
    * {{:magistraleinformatica:mod:08-domains-draft-2016.pdf|Chapter 8}}: Domain theory (draft)
      * P179, line 2: (d<sub>i</sub>,e<sub>i</sub>) should be {(d<sub>i</sub>,e<sub>i</sub>)}
    * {{:magistraleinformatica:mod:09-hofl-densem-draft-2016.pdf|Chapter 9}}: Denotational semantics of HOFL (draft)
      * P202, line 1: induction should be inductive
    * {{:magistraleinformatica:mod:10-hofl-semeq-draft-2016.pdf|Chapter 10}}: Equivalence between the operational and denotational semantics of HOFL (draft)
    * {{:magistraleinformatica:mod:11-ccs-draft-2016.pdf|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<sub>m</sub>) should be (p',q<sub>m</sub>)
      * P256, explanation of diamond op: satisfies and the should be satisfies the
      * P264, item 1: string should be strong
    * {{:magistraleinformatica:mod:12-ltl-ctl-mu-draft-2016-new.pdf|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
    * {{:magistraleinformatica:mod:13-pi-draft-2016.pdf|Chapter 13}}: Pi-calculus (draft)
      * P289, abstract: ingenuous should be ingenious
    * {{:magistraleinformatica:mod:14-markov-draft-2016_copia.pdf|Chapter 14}}: Measure Theory and Markov Chains (draft)
      * P320, line-9: X<sub>1</sub> should be X<sub>t</sub>
      * P322, end of last line: a<sub>i,i+1</sub> should be a<sub>si,si+1</sub>
      * P326, line -12: \mu should be l (twice)
      * P328, mid page: \gamma_M should be \gamma_D
    * {{:magistraleinformatica:mod:15-markov-action-nondet-draft-2016.pdf|Chapter 15}}: Discrete Time Markov Chains with Actions and Non-determinism (draft)
    * {{:magistraleinformatica:mod:16-pepa-draft-2016.pdf|Chapter 16}}: PEPA (draft, optional reading)