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