CS 611: Course Handouts

• Course Syllabus:
  • administrative information
  • course prerequisites
  • resource information
  • homework and exam information
  • some practical advice
• Papers regarding applications of axiomatic semantics:
  • Proof-Carrying Code George C. Necula, Presented at POPL97.
  • Safe Kernel Extensions Without Run-Time Checking George C. Necula, Peter Lee, Presented at OSDI'96.
• Type Systems, a paper by Luca Cardelli about why types are a good idea.
• Final Exam (dvi)
• bug fix 1 (Mon 1:27pm): Figure 1 now includes the appropriate rules for the operational semantics for regular expressions.
• clarification (Mon 1:27pm) on problem 2b: Prove that if (R,s,nil) evaluates to b, then (b = true iff s is in R[R])
• bug fix 2 (Tue 2:33pm): In question 2e, that should've read: "Your function should have the property that if (R,s,nil) evaluates to b, then the ML expression match R s (fun [] => true | fn _ => false) should evaluate to b. (I had "reg" instead of "match").
• bug fix 3 (Tue 2:33pm): Questions 3a and 3b were not stated properly. They should've read:

  (a) If |- e : int, e = E[i], and E[I] -> e', then |- e' : int.

  (b) If |- e : int, then either e = i or else there exists an E, I, and e' such that e = E[I] and E[I] -> e'.

• bug fix 4 (Wed 3:29pm): Figure 2. We need a technical side condition that the variable used to plug the whole in the continuation is "fresh" (i.e., does not occur elsewhere in the context.)