CORRECTIONS AND CLARIFICATIONS FOR LECTURE NOTES ON SEMANTICS OF PROGRAMMING LANGAUGAGES. Sam Staton. Last updated April 23 2010. Many thanks to (in no meaningful order): Jakub Kaplan, Vaiva Imbrasaite, Andrius Aucinas, Richard Whitehouse, Sebastian Probst-Eide, Alan Aralbeyev, Hassan Hamad, Chris Smowdon, Jon Wickerson, Karoliina Lehtinen, Rasmus Kyng, Qi Bill Chen and ChloĆ« Brown. Page 4. Suggested exercises. Exercise 10 requires Exercise 9. Page 9. The Ruby example in the notes has been corrupted. In the lecture I used these two example programs: def applydouble(y) yield(y*2) end x = 123 puts "x is #{x}" applydouble(7) {|x| puts x } puts "x is #{x}" versus def applydouble(y) yield(y*2) end x = 123 puts "x is #{x}" applydouble(7) {|z| puts z } puts "x is #{x}" You might expect them to do the same thing, but up to Ruby 1.9 they give different results. (Thanks to Sebastian Probst-Eide for Ruby advice.) Page 24. "Typeability problem" would better be called "Type Inference problem", because you may be able to prove that a term is typable without actually exhibiting a type. Page 30 Exercise 3. The first L1 example is the one on Slide 14. Exercise 9. For assign1' and seq1', see Slide 37 not Slide 38. Page 34. At the top of the page. In the definition of Abstract Syntax Trees, := is NOT a binary node in L1/L2. Rather, l:= is a unary node, for each location l. Page 44. Below the proof of Lemma 14, should read Now prove the first part, ie if Gamma |- e:T and dom(Gamma) subseteq dom(s) rather than Now prove the first part, ie if Gamma |- e:T and dom(Gamma) SUPseteq dom(s) . Page 44. In the proof of Theorem 3, case op1, the third line says "and dom(Gamma) subseteq dom(Gamma)". It should say "and dom(Gamma) subseteq dom(s)". Page 47. At the bottom of the page. NB "first-order" is defined differently by different people. This is the definition that we are taking in this course. Page 67. Exercise 21. "First-order" is defined at the bottom of page 47. Exercise 22, second sentence. "Is it possible to do it without using the store?" Page 75. Slide 166. Theorem 19 is true, but it is not strong enough to prove the safety property. I handed out a revised version of Slide 166 in Lecture 10. Please contact me if you did not get a copy. Page 88. Exercise 32. The bogus subtype rules are not on page 6! They are on slide 183 on page 85. Page 90. Slide 199 is missing "end end" at the end of the definitions of f and g. Page 91. Slide 203 could do with some explanation in the narrative. It is included as it is used in the argument as to why the Semantic Equivalence for L1 (Slide 202) satisfies condition 5 on Slide 201. If you equated programs that changed the store in DIFFERENT ways, then you could use the contexts on Slide 203 to distinguish them; so Condition 4 on Slide 201 would not hold. Page 93. Slide 206: "forall s" should be "for all s". Page 94. In Slide 210, the final three lines should read (a) -->w and -->w, or (b) for some s1 and s2 we have -->* and -->* . Page 97. Slide 219 onwards: we are using () instead of skip. (This is the ML notation for skip.) Please let me know anything else you spot! sam dot staton at cl dot cam dot ac dot uk