 Understand the lecture slides and discussions thoroughly.
 Revisit the MPs and HWs and make sure you understand the solutions
thoroughly. Repeat any you are not comfortable with.
 Take the sample exam as a dryrun for the actual exam.
The exam will cover all the lectures in the course. It is a
comprehansive exam. Listed here are topics not previously listed
in midterm1.syllabus.html or
midterm2.syllabus.html.
They include
Natural Semantics and
Transition Semantics,
Lambda Calculus, Evaluation
strategies (eager and lazy evaluation),
and Axiomatic Semantics. The following give
examples of the kinds of
questions you are likely to be asked for each topic:
Operational Semantics
 Be able to derive the proof tree for the evaluation of an expression in Natural semantics.
 Be able to derive the proof tree for the evaluation of an expression in Transition semantics.
 Be able to compare Natural and Transition semantics.
 Understand the evaluation rules in both semantics, and be able to
write evaluation rules for new syntactic constructs.
 Be able to implement Natural and Transition semantics rules as
OCaml programs.
Lambda Calculus (LC)
 Be able to parse a lambda term correctly (e.g. which
variable is bound by which abstraction, which variable is
free, which application is topmost, etc.)
 Describe and know how to apply αconversions
and βreductions.
 Know the differences between and be able to
demonstrate lazy/eager evaluation and unrestricted
alphabeta reduction.
Axiomatic Semantics
 Be able to prove simple statements in FloydHoare Logic, similar
to the example of if x < 0 then y:= yx else y:= y+x
{y=a+x} that was done in class.
